%------------------------------------------------------------------------------ %----Testing for $less_int % Status : Theorem fof(prove_2_less_3,conjecture,( $less_int(2,3) )). % Status : Theorem fof(prove_3_not_less_2,conjecture,( ~ $less_int(3,2) )). % Status : Theorem fof(prove_2_less_13,conjecture,( $less_int(2,13) )). % Status : Theorem fof(something_less_13,conjecture,( ? [X] : $less_int(X,13) )). % Status : Theorem fof(prove_12_less_something,conjecture,( ? [X] : $less_int(12,X) )). % Status : Theorem fof(something_less_something,conjecture,( ? [X,Y] : $less_int(X,Y) )). % Status : Theorem %----Order with negatives fof(n2_less_2,conjecture,( $less_int(-2,2) )). % Status : Theorem fof(n4_less_n2,conjecture,( $less_int(-4,-2) )). % Status : Theorem fof(prove_2_not_less_n2,conjecture,( ~ $less_int(2,-2) )). % Status : Theorem fof(n2_not_less_n4,conjecture,( ~ $less_int(-2,-4) )). % Status : Theorem fof(something_less_0,conjecture,( ? [X] : $less_int(X,0) )). % Status : Theorem fof(something_less_n2,conjecture,( ? [X] : $less_int(X,-2) )). % Status : Theorem fof(n2_less_something,conjecture,( ? [X] : $less_int(-2,X) )). %------------------------------------------------------------------------------ %----Testing for $lesseq_int % Status : Theorem fof(prove_2_lesseq_2,conjecture,( $lesseq_int(2,2) )). % Status : Theorem fof(prove_2_lesseq_3,conjecture,( $lesseq_int(2,3) )). % Status : Theorem fof(prove_3_not_lesseq_2,conjecture,( ~ $lesseq_int(3,2) )). % Status : Theorem fof(something_lesseq_13,conjecture,( ? [X] : $lesseq_int(X,13) )). % Status : Theorem fof(prove_12_lesseq_something,conjecture,( ? [X] : $lesseq_int(12,X) )). % Status : Theorem fof(something_lesseq_something,conjecture,( ? [X,Y] : $lesseq_int(X,Y) )). %----Order with negatives % Status : Theorem fof(n2_lesseq_n2,conjecture,( $lesseq_int(-2,-2) )). % Status : Theorem fof(n2_lesseq_2,conjecture,( $lesseq_int(-2,2) )). % Status : Theorem fof(n4_lesseq_n2,conjecture,( $lesseq_int(-4,-2) )). % Status : Theorem fof(prove_2_not_lesseq_n2,conjecture,( ~ $lesseq_int(2,-2) )). % Status : Theorem fof(n2_not_lesseq_n4,conjecture,( ~ $lesseq_int(-2,-4) )). % Status : Theorem fof(something_lesseq_0,conjecture,( ? [X] : $lesseq_int(X,0) )). % Status : Theorem fof(something_lesseq_n2,conjecture,( ? [X] : $lesseq_int(X,-2) )). % Status : Theorem fof(n2_lesseq_something,conjecture,( ? [X] : $lesseq_int(-2,X) )). %------------------------------------------------------------------------------ %----Testing for Inequality % Status : Theorem fof(prove_31_not_12,conjecture,( 31 != 21 )). % Status : Theorem fof(something_not_12,conjecture,( ? [X] : X != 12 )). %------------------------------------------------------------------------------ %----Testing for $plus_int % Status : Theorem fof(sum_2_3_5,conjecture,( $plus_int(2,3) = 5 )). % Status : Theorem fof(sum_23_34_57,conjecture,( $plus_int(23,34) = 57 )). % Status : Theorem fof(sum_23_34_something,conjecture,( ? [X] : $plus_int(23,34) = X )). % Status : Theorem fof(sum_something_23_34,conjecture,( ? [X] : $plus_int(X,23) = 34 )). % Status : Theorem fof(sum_23_something_34,conjecture,( ? [X] : $plus_int(23,X) = 34 )). % Status : Theorem fof(sum_2_3_not_6,conjecture,( $plus_int(2,3) != 6 )). % Status : Theorem fof(sum_2_3_only_5,conjecture,( ! [X] : ( $plus_int(2,3) = X => X = 5 ) )). % Status : Theorem fof(sum_only_2_3_5,conjecture,( ! [X] : ( $plus_int(X,3) = 5 => X = 2 ) )). % Status : Theorem fof(sum2_only_3_5,conjecture,( ! [X] : ( $plus_int(2,X) = 5 => X = 3 ) )). % Status : Theorem fof(sum_n2_n5_n7,conjecture,( $plus_int(-2,-5) = -7 )). % Status : Theorem fof(sum_2_n5_n3,conjecture,( $plus_int(2,-5) = -3 )). % Status : Theorem fof(sum_5_n2_3,conjecture,( $plus_int(5,-2) = 3 )). % Status : Theorem fof(sum_5_n5_0,conjecture,( $plus_int(5,-5) = 0 )). % Status : Theorem fof(sum_n2_n5_what,conjecture,( ? [X] : $plus_int(-2,-5) = X )). % Status : Theorem fof(sum_2_n5_what,conjecture,( ? [Y] : $plus_int(2,-5) = Y )). % Status : Theorem fof(sum_5_n2_what,conjecture,( ? [X] : $plus_int(5,-2) = X )). % Status : Theorem fof(sum_5_n5_what,conjecture,( ? [X] : $plus_int(5,-5) = X )). % Status : Theorem fof(sum_what_n5_n7,conjecture,( ? [X] : $plus_int(X,-5) = -7 )). % Status : Theorem fof(sum_what_n5_n3,conjecture,( ? [X] : $plus_int(X,-5) = -3 )). % Status : Theorem fof(sum_what_n2_3,conjecture,( ? [X] : $plus_int(X,-2) = 3 )). % Status : Theorem fof(sum_what_n5_0,conjecture,( ? [X] : $plus_int(X,-5) = 0 )). % Status : Theorem fof(sum_zero_identity,conjecture,( ? [X] : $plus_int(X,0) = X )). % Status : Theorem fof(sum_something_anotherthing_firstthing,conjecture,( ? [X,Y] : $plus_int(X,Y) = X )). % Status : Theorem fof(idempotent_element,conjecture,( ? [X] : $plus_int(X,X) = X )). % Status : Theorem fof(sum_4_4_8,conjecture,( ? [X,Y] : ( $plus_int(X,Y) = 8 & X = 4 & Y = 4 ) )). % Status : Theorem fof(communative_sum_6_7,conjecture,( ! [Z1,Z2] : ( ( $plus_int(6,7) = Z1 & $plus_int(7,6) = Z2 ) => Z1 = Z2 ) )). % Status : Theorem fof(associative_sum,conjecture,( ! [Z1,Z2,Z3,Z4] : ( ( $plus_int(2,3) = Z1 & $plus_int(Z1,6) = Z2 & $plus_int(3,6) = Z3 & $plus_int(2,Z3) = Z4 ) => Z2 = Z4 ) )). % Status : Theorem fof(associative,conjecture,( ? [X,Y,Z,Z1,Z2,Z3,Z4] : ( ( $plus_int(X,Y) = Z1 & $plus_int(Z1,Z) = Z2 & $plus_int(Y,Z) = Z3 & $plus_int(X,Z3) = Z4 ) => Z2 = Z4 ) )). % Status : Theorem fof(associative,conjecture,( ! [X,Y,Z,Z1,Z2,Z3,Z4] : ( ( $plus_int(X,Y) = Z1 & $plus_int(Z1,Z) = Z2 & $plus_int(Y,Z) = Z3 & $plus_int(X,Z3) = Z4 ) => Z2 = Z4 ) )). % Status : Theorem fof(sum_2_3_5_predicate,conjecture,( p($plus_int(2,3)) => p(5) )). % Status : Theorem fof(sum_X_Y_5_predicate,conjecture,( ( ( p(3,4) & ~ p(1,6) ) => ? [X,Y] : ( p(X,Y) & $plus_int(X,Y) = 7 ) ) )). % Status : Theorem fof(prove_0_identity,conjecture,( ! [X] : $plus_int(X,0) = X )). % Status : Theorem fof(prove_0_identity_rev,conjecture,( ! [X] : $plus_int(0,X) = X )). % Status : CounterSatisfiable fof(anti_sum_2_2_5,conjecture,( $plus_int(2,2) = 5 )). % Status : CounterSatisfiable fof(anti_sum_x_x_y,conjecture,( ! [X,Y] : $plus_int(X,X) = Y )). % Status : CounterSatisfiable fof(anti_sum_x_y_x,conjecture,( ! [X,Y] : $plus_int(X,Y) = X )). % Status : CounterSatisfiable fof(anti_unique,conjecture,( ? [X,Y,Z1,Z2] : ( $plus_int(X,Y) = Z1 & $plus_int(X,Y) = Z2 & Z1 != Z2 ) )). % Status : CounterSatisfiable fof(anti_associativity,conjecture,( ? [X,Y,Z,Z1,Z2,Z3,Z4] : ( $plus_int(X,Y) = Z1 & $plus_int(Z1,Z) = Z2 & $plus_int(Z,X) = Z3 & $plus_int(Z3,Y) = Z4 & Z2 != Z4 ) )). % Status : CounterSatisfiable fof(what_what_0,conjecture,( ? [X] : ( X != 0 & $plus_int(X,X) = 0 ) )). % Status : CounterSatisfiable fof(anti_sum_only_4_only_4_8,conjecture,( ! [X,Y] : ( $plus_int(X,Y) = 8 => ( X = 4 & Y = 4 ) ) )). % Status : CounterSatisfiable fof(anti_sum_identity,conjecture,( ? [X] : $plus_int(X,0) != X )). % Status : CounterSatisfiable fof(anti_sum_identity,conjecture,( ? [X,Y] : ( $plus_int(X,0) = Y & Y != X ) )). % Status : CounterSatisfiable fof(anti_sum_idempotence,conjecture,( ! [X] : $plus_int(X,X) = X )). % Status : CounterSatisfiable fof(anti_not_sum_idempotence,conjecture,( ! [X] : $plus_int(X,X) != X )). %------------------------------------------------------------------------------ %----Testing for $minus_int % Status : Theorem fof(diff_7_5_2,conjecture,( $minus_int(7,5) = 2 )). % Status : Theorem fof(diff_5_3_only_2,conjecture,( ! [X] : ( $minus_int(5,3) = X => X = 2 ) )). % Status : Theorem fof(diff_only_5_2_3,conjecture,( ! [X] : ( $minus_int(X,2) = 3 => X = 5 ) )). % Status : Theorem fof(diff_5_only_3_2,conjecture,( ! [X] : ( $minus_int(5,X) = 2 => X = 3 ) )). % Status : Theorem fof(diff_zero_identity,conjecture,( ? [X] : $minus_int(X,0) = X )). % Status : Theorem fof(diff_5_3_2_predicate,conjecture,( p($minus_int(5,3)) => p(2) )). % Status : Theorem fof(anti_lower_boundary,conjecture,( ? [X] : $minus_int(-128,1) = X )). % Status : Theorem fof(x_minus_x_equals_0,conjecture,( ! [X] : $minus_int(X,X) = 0 )). % Status : Theorem fof(identity,conjecture,( ! [X,Y] : ( $minus_int(X,Y) = 0 => X = Y ) )). %------------------------------------------------------------------------------ %----Testing for $times_int % Status : Theorem fof(times_2_3_6,conjecture,( $times_int(2,3) = 6 )). % Status : Theorem fof(times_n2_3_n6,conjecture,( $times_int(-2,3) = -6 )). % Status : Theorem fof(times_n2_n3_6,conjecture,( $times_int(-2,-3) = 6 )). % Status : Theorem fof(times_11_11_121,conjecture,( $times_int(11,11) = 121 )). % Status : Theorem fof(times_11_11_something,conjecture,( ? [X] : $times_int(11,11) = X )). % Status : Theorem fof(times_something_11_121,conjecture,( ? [X] : $times_int(X,11) = 121 )). % Status : Theorem fof(times_11_something_121,conjecture,( ? [X] : $times_int(11,X) = 121 )). % Status : Theorem fof(times_2_3_not_5,conjecture,( $times_int(2,3) != 5 )). % Status : Theorem fof(times_2_3_only_6,conjecture,( ! [X] : ( $times_int(2,3) = X => X = 6 ) )). % Status : Theorem fof(times_only_2_3_6,conjecture,( ! [X] : ( $times_int(X,3) = 6 => X = 2 ) )). % Status : Theorem fof(times_2_only_3_5,conjecture,( ! [X] : ( $times_int(2,X) = 6 => X = 3 ) )). % Status : Theorem fof(times_n2_n5_n7,conjecture,( $times_int(-2,-5) = 10 )). % Status : Theorem fof(times_2_n5_n3,conjecture,( $times_int(2,-5) = -10 )). % Status : Theorem fof(times_5_n2_3,conjecture,( $times_int(5,-2) = -10 )). % Status : Theorem fof(times_5_0_0,conjecture,( $times_int(5,0) = 0 )). % Status : Theorem fof(times_n2_n5_what,conjecture,( ? [X] : $times_int(-2,-5) = X )). % Status : Theorem fof(times_2_n5_what,conjecture,( ? [Y] : $times_int(2,-5) = Y )). % Status : Theorem fof(times_5_n2_what,conjecture,( ? [X] : $times_int(5,-2) = X )). % Status : Theorem fof(times_what_n5_n7,conjecture,( ? [X] : $times_int(X,-5) = -10 )). % Status : Theorem fof(times_what_n5_n3,conjecture,( ? [X] : $times_int(X,-5) = 10 )). % Status : Theorem fof(times_zero_identity,conjecture,( ? [X] : $times_int(X,0) = 0 )). % Status : Theorem fof(times_1_identity,conjecture,( ? [X] : $times_int(X,1) = X )). % Status : Theorem fof(times_something_anotherthing_firstthing,conjecture,( ? [X,Y] : $times_int(X,Y) = X )). % Status : Theorem fof(idempotent_element,conjecture,( ? [X] : $times_int(X,X) = X )). % Status : Theorem fof(times_4_4_8,conjecture,( ? [X,Y] : ( $times_int(X,Y) = 16 & X = 4 & Y = 4 ) )). % Status : Theorem fof(times_X_X_4_predicate,conjecture,( ( p(2) => ? [X,Y] : ( p(X) & X != Y & $times_int(Y,Y) = 4 ) ) )). % Status : Theorem fof(communative_times_6_7,conjecture,( ! [Z1,Z2] : ( ( $times_int(6,7) = Z1 & $times_int(7,6) = Z2 ) => Z1 = Z2 ) )). % Status : Theorem fof(associative_sum,conjecture,( ! [Z1,Z2,Z3,Z4] : ( ( $times_int(2,3) = Z1 & $times_int(Z1,6) = Z2 & $times_int(3,6) = Z3 & $times_int(2,Z3) = Z4 ) => Z2 = Z4 ) )). % Status : Theorem fof(associative,conjecture,( ? [X,Y,Z,Z1,Z2,Z3,Z4] : ( ( $times_int(X,Y) = Z1 & $times_int(Z1,Z) = Z2 & $times_int(Y,Z) = Z3 & $times_int(X,Z3) = Z4 ) => Z2 = Z4 ) )). % Status : Theorem fof(times_5_3_15_predicate,conjecture,( p($times_int(5,3)) => p(15) )). % Status : CounterSatisfiable fof(anti_times_2_2_5,conjecture,( $times_int(2,2) = 5 )). % Status : CounterSatisfiable fof(anti_times_x_x_y,conjecture,( ! [X,Y] : $times_int(X,X) = Y )). % Status : CounterSatisfiable fof(anti_times_x_y_x,conjecture,( ! [X,Y] : $times_int(X,Y) = X )). % Status : CounterSatisfiable fof(anti_unique,conjecture,( ? [X,Y,Z1,Z2] : ( $times_int(X,Y) = Z1 & $times_int(X,Y) = Z2 & Z1 != Z2 ) )). % Status : CounterSatisfiable fof(anti_associativity,conjecture,( ? [X,Y,Z,Z1,Z2,Z3,Z4] : ( $times_int(X,Y) = Z1 & $times_int(Z1,Z) = Z2 & $times_int(Z,X) = Z3 & $times_int(Z3,Y) = Z4 & Z2 != Z4 ) )). % Status : CounterSatisfiable fof(what_what_0,conjecture,( ? [X] : ( X != 0 & $times_int(X,X) = 0 ) )). % Status : CounterSatisfiable fof(anti_times_only_2_only_4_8,conjecture,( ! [X,Y] : ( $times_int(X,Y) = 8 => ( X = 2 & Y = 4 ) ) )). % Status : CounterSatisfiable fof(anti_times_identity,conjecture,( ? [X] : $times_int(X,1) != X )). % Status : CounterSatisfiable fof(anti_times_identity,conjecture,( ? [X,Y] : ( $times_int(X,1) = Y & Y != X ) )). % Status : CounterSatisfiable fof(anti_times_idempotence,conjecture,( ! [X] : $times_int(X,X) = X )). % Status : CounterSatisfiable fof(anti_not_times_idempotence,conjecture,( ! [X] : $times_int(X,X) != X )). % Status : CounterSatisfiable fof(prove_0_identity,conjecture,( ! [X] : $times_int(X,0) = X )). % Status : CounterSatisfiable fof(prove_0_identy_rev,conjecture,( ! [X] : $times_int(0,X) = X )). %------------------------------------------------------------------------------ %----Testing for $divide_int % Status : Theorem fof(divide_15_5_3,conjecture,( $divide_int(15,5) = 3 )). % Status : Theorem fof(divide_15_n5_n3,conjecture,( $divide_int(15,-5) = -3 )). % Status : Theorem fof(divide_n15_5_n3,conjecture,( $divide_int(-15,5) = -3 )). % Status : Theorem fof(divide_n15_n5_3,conjecture,( $divide_int(-15,-5) = 3 )). % Status : Theorem fof(divide_15_3_only_5,conjecture,( ! [X] : ( $divide_int(15,3) = X => X = 5 ) )). % Status : Theorem fof(divide_15_n3_only_n5,conjecture,( ! [X] : ( $divide_int(15,-3) = X => X = -5 ) )). % Status : Theorem fof(divide_14_only_7_2,conjecture,( ! [X] : ( $divide_int(14,X) = 2 => X = 7 ) )). % Status : Theorem fof(divide_zero_identity,conjecture,( ? [X] : $divide_int(X,1) = X )). % Status : Theorem fof(divide_15_3_5_predicate,conjecture,( p($divide_int(15,3)) => p(5) )). % Status : CounterSatisfiable fof(divide_only_12_2_6,conjecture,( ! [X] : ( $divide_int(X,2) = 6 => X = 12 ) )). % Status : CounterSatisfiable fof(x_divide_x_equals_0,conjecture,( ! [X] : $divide_int(X,X) = 0 )). % Status : CounterSatisfiable fof(identity,conjecture,( ! [X,Y] : ( $divide_int(X,Y) = 0 => X = Y ) )). %------------------------------------------------------------------------------ %----Testing for $remainder_int % Status : Theorem fof(remainder_15_4_3,conjecture,( $remainder_int(15,4) = 3 )). % Status : Theorem fof(remainder_15_n4_n3,conjecture,( $remainder_int(15,-4) = 3 )). % Status : Theorem fof(remainder_n15_4_n3,conjecture,( $remainder_int(-15,4) = -3 )). % Status : Theorem fof(remainder_n15_n4_3,conjecture,( $remainder_int(-15,-4) = -3 )). % Status : Theorem fof(remainder_15_4_only_3,conjecture,( ! [X] : ( $remainder_int(15,4) = X => X = 3 ) )). % Status : Theorem fof(remainder_n1_exists,conjecture,( ? [X] : $remainder_int(X,1) = 0 )). % Status : Theorem fof(remainder_X_1_0,conjecture,( ! [X] : $remainder_int(X,1) = 0 )). % Status : Theorem fof(remainder_15_4_3_predicate,conjecture,( p($remainder_int(15,4)) => p(3) )). % Status : Theorem fof(remainder_X_X_0,conjecture,( ! [X] : ( X != 0 => $remainder_int(X,X) = 0 ) )). % Status : CounterSatisfiable fof(unique_remainder_0,conjecture,( ! [X,Y] : ( X != 0 => ( $remainder_int(X,Y) = 0 => X = Y ) ) )). %------------------------------------------------------------------------------ %----Testing for $uminus_int % Status : Theorem fof(n2_equal_uminus_2,conjecture,( -2 = $uminus_int(2) )). % Status : Theorem fof(n2_equal_uminus_n2,conjecture,( 2 = $uminus_int(-2) )). % Status : Theorem fof(sum_2_uminus_to_0,conjecture,( $plus_int(2,$uminus_int(2)) = 0 )). % Status : Theorem fof(sum_n2_uminus_to_0,conjecture,( $plus_int(-2,$uminus_int(-2)) = 0 )). % Status : Theorem fof(uminus_uminus_2,conjecture,( $uminus_int($uminus_int(2)) = 2 )). % Status : Theorem fof(uminus_uminus_n2,conjecture,( $uminus_int($uminus_int(-2)) = -2 )). % Status : Theorem fof(uminus_uminus,conjecture,( ! [X] : $uminus_int($uminus_int(X)) = X )). % Status : Theorem fof(sum_uminus_to_0,conjecture,( ! [X] : $plus_int(X,$uminus_int(X)) = 0 )). % Status : Theorem fof(uminus_equal,conjecture,( ! [X] : ( X = $uminus_int(X) <=> X = 0 ) )). %------------------------------------------------------------------------------ %----Testing for combinations % Status : Theorem fof(less_lesseq,conjecture,( ! [X,Y] : ( $lesseq_int(X,Y) <=> ( $less_int(X,Y) | X = Y ) ) )). % Status : Theorem fof(add_same_as_subtract,conjecture,( ? [X,Y,Z] : ( $plus_int(X,Y) = Z <=> ( $minus_int(Z,Y) = X & $minus_int(Z,X) = Y ) ) )). % Status : Theorem fof(sum_and_difference,conjecture,( ? [X,Y] : ( $plus_int(X,Y) = 8 & $minus_int(X,Y) = 0 ) )). % Status : Theorem fof(sum_something_0_samething,conjecture,( ! [X] : ( ( $less_int(-1,X) & $less_int(X,1) ) => $plus_int(21,X) = 21 ) )). % Status : Theorem fof(exist_bigger_plus_one,conjecture,( ? [X,Y] : ( $plus_int(X,1) = Y & $less_int(X,Y) ) )). % Status : Theorem fof(sum_2_3_less_6,conjecture,( ! [X] : ( $plus_int(2,3) = X => $less_int(X,6) ) )). % Status : Theorem fof(sum_2_3_greater_4,conjecture,( ! [X] : ( $plus_int(2,3) = X => $less_int(4,X) ) )). % Status : Theorem fof(complex1,conjecture,( ? [X] : X = $plus_int($times(2,-3),divide_int($uminus_int(-8),4)) )). % Status : Theorem fof(complex2,conjecture,( $less_int($times_int(-4,$minus(127,99)),$plus($uminus_int(3),27)) )). % Status : Theorem %----Successive integers fof(less_successor,conjecture,( ! [X,Z] : ( $less_int(Z,$plus_int(X,1)) => $lesseq_int(Z,X) ) )). % Status : Theorem fof(plus_minus,conjecture,( ! [X,Y,Z] : ( $plus_int(X,Y) = Z => $minus_int(Z,X) = Y ) )). % Status : Theorem fof(times_divide,conjecture,( ! [X,Y,Z] : ( ( X != 0 & $times_int(X,Y) = Z ) => $divide_int(Z,X) = Y ) )). % Status : CounterSatisfiable fof(exists_sum_consecutive_8,conjecture,( ? [X,Y] : ( $plus_int(X,Y) = 8 & $minus_int(X,Y) = 1 ) )). % Status : CounterSatisfiable fof(all_sum_consecutive_8,conjecture,( ! [X,Y] : ( $plus_int(X,Y) = 8 => $minus_int(X,Y) = 1 ) )). % Status : CounterSatisfiable fof(all_sum_same_8,conjecture,( ! [X,Y] : ( $plus_int(X,Y) = 8 => $minus_int(X,Y) = 0 ) )). % Status : CounterSatisfiable fof(sum_larger,conjecture,( ! [X,Y,Z] : ( $plus_int(X,Y) = Z => ( $less_int(X,Z) & $less_int(Y,Z) ) ) )). % Status : CounterSatisfiable fof(anti_sum_diff_less_1,conjecture,( ! [X,Y,Z1,Z2] : ( $plus_int(X,Y) = Z1 & $minus_int(X,Y) = Z2 & $less_int(Z1,Z2) ) )). % Status : CounterSatisfiable fof(anti_sum_diff_less_2,conjecture,( ! [X,Y,Z1,Z2] : ( $plus_int(X,Y) = Z1 & $minus_int(X,Y) = Z2 & $less_int(Z2,Z1) ) )). % Status : CounterSatisfiable fof(anti_sum_2_3_greater_7,conjecture,( ! [X] : ( $plus_int(2,3) = X => $less_int(7,X) ) )). % Status : CounterSatisfiable fof(x_plus_y_greater_x_minus_y,conjecture,( ! [X,Y,Z1,Z2] : ( ( $plus_int(X,Y) = Z1 & $minus_int(X,Y) = Z2 ) => $less_int(Z2,Z1) ) )). % Status : Theorem fof(difference_greater,conjecture,( ! [X,Y,Z] : ( ( $minus_int(X,Y) = Z & $less_int(0,Z) ) => $less_int(Y,X) ) )). %------------------------------------------------------------------------------ %----Problems from Uwe Waldman. He says ... %----Here are some problems for the integer arithmetic collection %----in TPTP. I hope I didn't introduce any bugs during the manual %----conversion to TPTP syntax. %---- %----Current status of the problems: We can solve the first three %----with SPASS+T; we can solve the fourth one if we add the %----additional axiom "! [X,Y] : $plus_int($minus_int(X,Y),Y) = X". %----Solving number five would require a rather nasty extension of %----SPASS+T. The sixth problem is way beyond anything we can do. % Status : Theorem fof(decreasing_pointer_list,conjecture, ( ( ! [X,Z] : ( ~ iselem(X) | data(X) != Z | $less_int(0,Z) ) & ! [X,Y] : ( ~ iselem(X) | ~ iselem(Y) | next(X) != Y | $less_int(data(Y),data(X)) ) & iselem(a) & iselem(next(a)) & iselem(next(next(a))) ) => $lesseq_int(3,data(a)) )). % Status : Theorem fof(sublist_of_oddnumbered_elements,conjecture, ( ( ! [X] : ( iselem(X) | length(X) = 0 ) & ! [X] : ( ~ iselem(X) | $lesseq_int(1,length(X)) ) & ! [X] : ( ~ iselem(X) | length(X) = $plus_int(length(next(X)),1) ) & ! [X] : ( iselem(X) <=> iselem(split1(X)) ) & ! [X] : ( ~ iselem(X) | data(split1(X)) = data(X) ) & ! [X] : ( ~ iselem(X) | ~ iselem(next(split1(X))) | iselem(next(X)) ) & ! [X] : ( ~ iselem(X) | ~ iselem(next(X)) | next(split1(X)) = split1(next(next(X))) ) & iselem(b) & iselem(next(b)) & next(next(b)) = a & ( $times_int(2,length(split1(a))) = $plus_int(length(a),1) | $times_int(2,length(split1(a))) = length(a) ) ) => ( $times_int(2,length(split1(b))) = $plus_int(length(b),1) | $times_int(2,length(split1(b))) = length(b) ) )). % Status : Theorem fof(boyer_moore_max_min,conjecture, ( ( ! [X] : $lesseq_int(min(X),max(X)) & $lesseq_int(l,min(a)) & $less_int(0,k) ) => $less_int(l,$plus_int(max(a),k)) )). % Status : Theorem fof(monotone_function,conjecture, ( ( ! [X] : $lesseq_int(f($plus_int(X,1)),f($plus_int(X,2))) & $lesseq_int(f(7),3) ) => $lesseq_int(f(4),3) )). % Status : Theorem fof(injective_f_pigeonhole,conjecture, ( ( ! [X,Y] : ( f(X) = f(Y) => X = Y ) & $less_int(6,f(3)) & $less_int(f(3),9) & $less_int(6,f(4)) & $less_int(f(4),9) ) => ( $lesseq_int(f(5),6) | $lesseq_int(9,f(5)) ) )). % Status : Theorem fof(fxxx_is_either_even_or_odd,conjecture, ( ? [X,Y,Z] : f(X,X,Y) = $times_int(2,Z) | ? [X,Y,Z] : f(X,Y,Y) = $plus_int($times_int(2,Z),1) )). %------------------------------------------------------------------------------