| index | label | type | more | source | modified | indexed | | 1 | cnf(avoid_kangaroo,negated_conjecture,
( ~ avoided(the_kangaroo) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/PUZ/PUZ002-1/query.owl | 2008-07-03 | 2008-07-23 |
| 2 | cnf(a_not_equal_to_additive_identity_2,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(less_or_equal_3,negated_conjecture,
( less_or_equal(a,additive_identity) )).
cnf(not_less_or_equal_4,negated_conjecture,
( ~ less_or_equal(multiplicative_inverse(a),additive_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD088-1/query.owl | 2008-07-06 | 2008-07-23 |
| 3 | cnf(additive_inverse_equals_additive_identity_2,negated_conjecture,
( equalish(additive_inverse(a),additive_identity) )).
cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(a,additive_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD019-1/query.owl | 2008-07-06 | 2008-07-23 |
| 4 | cnf(a_group,negated_conjecture,
( group(f69,f70) )).
cnf(prove_there_is_a_homomorphism,negated_conjecture,
( ~ homomorphism(Y,f69,f70,f69,f70) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/GRP/GRP016-1/query.owl | 2008-07-08 | 2008-07-23 |
| 5 | cnf(a_not_equal_to_additive_identity_2,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(multiplicative_inverse_equals_additive_identity_3,negated_conjecture,
( equalish(multiplicative_inverse(a),additive_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD040-1/query.owl | 2008-07-06 | 2008-07-23 |
| 6 | cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(multiplicative_identity_equals_multiply_4,negated_conjecture,
( equalish(multiplicative_identity,multiply(b,multiplicative_inverse(a))) )).
cnf(a_not_equal_to_b_5,negated_conjecture,
( ~ equalish(a,b) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD038-1/query.owl | 2008-07-06 | 2008-07-23 |
| 7 | cnf(a_times_b,negated_conjecture,
( product(a,b,additive_identity) )).
cnf(a_not_additive_identity,negated_conjecture,
( a != additive_identity )).
cnf(prove_b_is_additive_identity,negated_conjecture,
( b != additive_identity )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/RNG/RNG041-1/query.owl | 2008-07-11 | 2008-07-23 |
| 8 | cnf(a_equals_b_5,negated_conjecture,
( equalish(a,b) )).
cnf(c_equals_d_6,negated_conjecture,
( equalish(c,d) )).
cnf(add_not_equal_to_add_7,negated_conjecture,
( ~ equalish(add(a,c),add(d,b)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD013-1/query.owl | 2008-07-06 | 2008-07-23 |
| 9 | cnf(add_not_equal_to_a_3,negated_conjecture,
( ~ equalish(add(a,add(b,additive_inverse(b))),a) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD003-1/query.owl | 2008-07-06 | 2008-07-23 |
| 10 | cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(b_not_equal_to_additive_identity_4,negated_conjecture,
( ~ equalish(b,additive_identity) )).
cnf(less_or_equal_5,negated_conjecture,
( less_or_equal(multiplicative_inverse(b),multiplicative_inverse(a)) )).
cnf(less_or_equal_6,negated_conjecture,
( less_or_equal(multiplicative_inverse(a),additive_identity) )).
cnf(not_less_or_equal_7,negated_conjecture,
( ~ less_or_equal(a,b) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD085-1/query.owl | 2008-07-06 | 2008-07-23 |
| 11 | cnf(antecedent,negated_conjecture,
( ordered(x,implies(y,z))
| ordered(y,implies(x,z)) )).
cnf(prove_wajsberg_theorem,negated_conjecture,
( ~ ordered(x,implies(y,z))
| ~ ordered(y,implies(x,z)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/LCL/LCL144-1/query.owl | 2008-04-13 | 2008-07-23 |
| 12 | cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(b_not_equal_to_additive_identity_4,negated_conjecture,
( ~ equalish(b,additive_identity) )).
cnf(add_not_equal_to_multiply_5,negated_conjecture,
( ~ equalish(add(multiplicative_inverse(a),multiplicative_inverse(b)),multiply(add(a,b),multiplicative_inverse(multiply(a,b)))) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD054-1/query.owl | 2008-07-06 | 2008-07-23 |
| 13 | n/a | Query | browser2 | http://inference-web.org/proofs/laptop/ex7.owl | 2007-11-14 | 2008-07-24 |
| 14 | cnf(add_equals_b_5,negated_conjecture,
( equalish(add(a,u),b) )).
cnf(add_equals_b_6,negated_conjecture,
( equalish(add(a,v),b) )).
cnf(u_not_equal_to_v_7,negated_conjecture,
( ~ equalish(u,v) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD016-1/query.owl | 2008-07-06 | 2008-07-23 |
| 15 | cnf(a_not_equal_to_additive_identity_2,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(less_or_equal_3,negated_conjecture,
( less_or_equal(a,additive_inverse(multiplicative_identity)) )).
cnf(not_less_or_equal_4,negated_conjecture,
( ~ less_or_equal(additive_inverse(multiplicative_identity),multiplicative_inverse(a)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD092-1/query.owl | 2008-07-06 | 2008-07-23 |
| 16 | cnf(a_equals_b_6,negated_conjecture,
( equalish(a,b) )).
cnf(c_equals_d_7,negated_conjecture,
( equalish(c,d) )).
cnf(add_equals_u_8,negated_conjecture,
( equalish(add(a,c),u) )).
cnf(add_not_equal_to_u_9,negated_conjecture,
( ~ equalish(add(d,b),u) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD013-2/query.owl | 2008-07-06 | 2008-07-23 |
| 17 | cnf(additive_inverse_equals_additive_inverse_3,negated_conjecture,
( equalish(additive_inverse(a),additive_inverse(b)) )).
cnf(a_not_equal_to_b_4,negated_conjecture,
( ~ equalish(a,b) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD015-1/query.owl | 2008-07-06 | 2008-07-23 |
| 18 | cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(multiply_equals_a_4,negated_conjecture,
( equalish(multiply(m,a),a) )).
cnf(m_not_equal_to_multiplicative_identity_5,negated_conjecture,
( ~ equalish(m,multiplicative_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD033-1/query.owl | 2008-07-06 | 2008-07-23 |
| 19 | cnf(a_equals_x_5,negated_conjecture,
( equalish(a,x) )).
cnf(add_equals_c_6,negated_conjecture,
( equalish(add(a,b),c) )).
cnf(add_not_equal_to_c_7,negated_conjecture,
( ~ equalish(add(x,b),c) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD017-1/query.owl | 2008-07-06 | 2008-07-23 |
| 20 | cnf(a_not_equal_to_additive_identity_6,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(b_not_equal_to_additive_identity_7,negated_conjecture,
( ~ equalish(b,additive_identity) )).
cnf(add_equals_u_8,negated_conjecture,
( equalish(add(multiplicative_inverse(a),multiplicative_inverse(b)),u) )).
cnf(add_equals_k_9,negated_conjecture,
( equalish(add(a,b),k) )).
cnf(multiply_equals_l_10,negated_conjecture,
( equalish(multiply(a,b),l) )).
cnf(multiply_not_equal_to_u_11,negated_conjecture,
( ~ equalish(multiply(k,multiplicative_inverse(l)),u) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD054-2/query.owl | 2008-07-06 | 2008-07-23 |
| 21 | cnf(a_equals_b_5,negated_conjecture,
( equalish(a,b) )).
cnf(c_equals_d_6,negated_conjecture,
( equalish(c,d) )).
cnf(multiply_not_equal_to_multiply_7,negated_conjecture,
( ~ equalish(multiply(a,c),multiply(d,b)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD025-1/query.owl | 2008-07-06 | 2008-07-23 |
| 22 | cnf(add_equals_add_4,negated_conjecture,
( equalish(add(a,c),add(b,c)) )).
cnf(a_not_equal_to_b_5,negated_conjecture,
( ~ equalish(a,b) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD022-1/query.owl | 2008-07-06 | 2008-07-23 |
| 23 | cnf(add_equals_u_7,negated_conjecture,
( equalish(add(a,c),u) )).
cnf(add_equals_v_8,negated_conjecture,
( equalish(add(d,b),v) )).
cnf(less_or_equal_9,negated_conjecture,
( less_or_equal(a,b) )).
cnf(less_or_equal_10,negated_conjecture,
( less_or_equal(c,d) )).
cnf(not_less_or_equal_11,negated_conjecture,
( ~ less_or_equal(u,v) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD061-2/query.owl | 2008-07-06 | 2008-07-23 |
| 24 | cnf(an_4,negated_conjecture,
( ~ is_a_theorem(or(not(or(a,a)),a)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/LCL/LCL005-1/query.owl | 2008-04-13 | 2008-07-23 |
| 25 | cnf(assumption_3_42,negated_conjecture,
( organization(sk1) )).
cnf(assumption_3_43,negated_conjecture,
( has_immunity(sk1,sk2) )).
cnf(assumption_3_44,negated_conjecture,
( ~ has_immunity(sk1,sk3) )).
cnf(assumption_3_45,negated_conjecture,
( ~ greater(hazard_of_mortality(sk1,sk3),hazard_of_mortality(sk1,sk2)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/MGT/MGT060-1/query.owl | 2008-07-06 | 2008-07-24 |
| 26 | cnf(a_not_equal_to_additive_identity_2,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(less_or_equal_3,negated_conjecture,
( less_or_equal(additive_identity,a) )).
cnf(not_less_or_equal_4,negated_conjecture,
( ~ less_or_equal(additive_identity,multiplicative_inverse(a)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD086-1/query.owl | 2008-07-06 | 2008-07-23 |
| 27 | cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(a_equals_b_4,negated_conjecture,
( equalish(a,b) )).
cnf(multiplicative_inverses_not_equal,negated_conjecture,
( ~ equalish(multiplicative_inverse(a),multiplicative_inverse(b)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD026-1/query.owl | 2008-07-06 | 2008-07-23 |
| 28 | cnf(a_not_additive_identity,negated_conjecture,
( a != additive_identity )).
cnf(prove_b_is_additive_identity,negated_conjecture,
( b != additive_identity )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/RNG/RNG038-1/query.owl | 2008-07-11 | 2008-07-23 |
| 29 | cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(b_not_equal_to_additive_identity_4,negated_conjecture,
( ~ equalish(b,additive_identity) )).
cnf(multiply_equals_additive_identity_5,negated_conjecture,
( equalish(multiply(a,b),additive_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD041-1/query.owl | 2008-07-06 | 2008-07-23 |
| 30 | cnf(additive_inverse_not_equal_to_a_2,negated_conjecture,
( ~ equalish(additive_inverse(additive_inverse(a)),a) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD007-1/query.owl | 2008-07-06 | 2008-07-23 |
| 31 | cnf(a_times_b,negated_conjecture,
( product(a,b,c) )).
cnf(b_times_a,negated_conjecture,
( product(b,a,d) )).
cnf(prove_c_equals_d,negated_conjecture,
( ~ equalish(c,d) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/RNG/RNG039-2/query.owl | 2008-07-11 | 2008-07-23 |
| 32 | cnf(a_equals_b_3,negated_conjecture,
( equalish(a,b) )).
cnf(additive_identity_not_equal_to_add_4,negated_conjecture,
( ~ equalish(additive_identity,add(b,additive_inverse(a))) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD023-1/query.owl | 2008-07-06 | 2008-07-23 |
| 33 | n/a | Query | browser2 | http://inference-web.org/proofs/laptop/ex11.owl | 2007-11-14 | 2008-07-24 |
| 34 | cnf(antecedent,negated_conjecture,
( ordered(x,y) )).
cnf(prove_wajsberg_theorem,negated_conjecture,
( ~ ordered(implies(z,x),implies(z,y)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/LCL/LCL143-1/query.owl | 2008-04-13 | 2008-07-23 |
| 35 | n/a | Query | browser2 | http://inference-web.org/proofs/wines/blandfishcolor.owl | 2007-11-14 | 2008-07-24 |
| 36 | cnf(add_equals_u_5,negated_conjecture,
( equalish(add(a,a),u) )).
cnf(add_equals_v_6,negated_conjecture,
( equalish(add(b,b),v) )).
cnf(less_or_equal_7,negated_conjecture,
( less_or_equal(a,b) )).
cnf(not_less_or_equal_8,negated_conjecture,
( ~ less_or_equal(u,v) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD060-2/query.owl | 2008-07-06 | 2008-07-23 |
| 37 | cnf(atlantic,negated_conjecture,
( ocean(atlantic) )).
cnf(indian,negated_conjecture,
( ocean(indian) )).
cnf(pacific,negated_conjecture,
( ocean(pacific) )).
cnf(southern,negated_conjecture,
( ocean(southern) )).
cnf(western_australia,negated_conjecture,
( state(western_australia) )).
cnf(northern_territory,negated_conjecture,
( state(northern_territory) )).
cnf(queensland,negated_conjecture,
( state(queensland) )).
cnf(south_australia,negated_conjecture,
( state(south_australia) )).
cnf(new_south_wales,negated_conjecture,
( state(new_south_wales) )).
cnf(victoria,negated_conjecture,
( state(victoria) )).
cnf(tasmania,negated_conjecture,
( state(tasmania) )).
cnf(wa_nt,negated_conjecture,
( borders(western_australia,northern_territory) )).
cnf(wa_sa,negated_conjecture,
( borders(western_australia,south_australia) )).
cnf(sa_nt,negated_conjecture,
( borders(south_australia,northern_territory) )).
cnf(sa_qld,negated_conjecture,
( borders(south_australia,queensland) )).
cnf(sa_nsw,negated_conjecture,
( borders(south_australia,new_south_wales) )).
cnf(sa_vic,negated_conjecture,
( borders(south_australia,victoria) )).
cnf(nt_qld,negated_conjecture,
( borders(northern_territory,queensland) )).
cnf(qld_nsw,negated_conjecture,
( borders(queensland,new_south_wales) )).
cnf(nsw_vic,negated_conjecture,
( borders(new_south_wales,victoria) )).
cnf(indian_wa,negated_conjecture,
( borders(indian,western_australia) )).
cnf(indian_nt,negated_conjecture,
( borders(indian,northern_territory) )).
cnf(indian_qld,negated_conjecture,
( borders(indian,queensland) )).
cnf(southern_wa,negated_conjecture,
( borders(southern,western_australia) )).
cnf(southern_sa,negated_conjecture,
( borders(southern,south_australia) )).
cnf(southern_vic,negated_conjecture,
( borders(southern,victoria) )).
cnf(southern_tas,negated_conjecture,
( borders(southern,tasmania) )).
cnf(pacific_qld,negated_conjecture,
( borders(pacific,queensland) )).
cnf(pacific_nsw,negated_conjecture,
( borders(pacific,new_south_wales) )).
cnf(pacific_vic,negated_conjecture,
( borders(pacific,victoria) )).
cnf(pacific_tas,negated_conjecture,
( borders(pacific,tasmania) )).
cnf(prove_borders,negated_conjecture,
( ~ state(State1)
| ~ state(State2)
| ~ borders(State1,State2)
| ~ borders(State1,Ocean)
| ~ borders(State2,Ocean)
| ~ ocean(Ocean) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/PUZ/PUZ022-1/query.owl | 2008-07-03 | 2008-07-23 |
| 38 | cnf(a_not_equal_to_additive_identity_2,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(less_or_equal_3,negated_conjecture,
( less_or_equal(additive_identity,multiplicative_inverse(a)) )).
cnf(not_less_or_equal_4,negated_conjecture,
( ~ less_or_equal(additive_identity,a) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD087-1/query.owl | 2008-07-06 | 2008-07-23 |
| 39 | cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(a_equals_b_4,negated_conjecture,
( equalish(a,b) )).
cnf(multiplicative_identity_not_equal_to_multiply_5,negated_conjecture,
( ~ equalish(multiplicative_identity,multiply(b,multiplicative_inverse(a))) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD037-1/query.owl | 2008-07-06 | 2008-07-23 |
| 40 | cnf(a_intersection_bDa,negated_conjecture,
( ~ intersection(a,bDa,aI_bDa) )).
cnf(prove_aI_bDa_is_empty,negated_conjecture,
( ~ member(A,aI_bDa) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/SET/SET008-1/query.owl | 2008-04-14 | 2008-07-23 |
| 41 | cnf(additive_inverse_not_equal_to_add_3,negated_conjecture,
( ~ equalish(additive_inverse(add(a,b)),add(additive_inverse(a),additive_inverse(b))) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD008-1/query.owl | 2008-07-06 | 2008-07-23 |
| 42 | cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(less_or_equal_4,negated_conjecture,
( less_or_equal(additive_identity,a) )).
cnf(less_or_equal_5,negated_conjecture,
( less_or_equal(a,b) )).
cnf(not_less_or_equal_6,negated_conjecture,
( ~ less_or_equal(multiplicative_inverse(b),multiplicative_inverse(a)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD082-1/query.owl | 2008-07-06 | 2008-07-23 |
| 43 | cnf(a_equals_b_3,negated_conjecture,
( equalish(a,b) )).
cnf(additive_inverse_not_equal_to_additive_inverse_4,negated_conjecture,
( ~ equalish(additive_inverse(a),additive_inverse(b)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD014-1/query.owl | 2008-07-06 | 2008-07-23 |
| 44 | cnf(a_times_b,negated_conjecture,
( product(a,b,c) )).
cnf(b_times_a,negated_conjecture,
( product(b,a,d) )).
cnf(prove_c_equals_d,negated_conjecture,
( c != d )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/RNG/RNG039-1/query.owl | 2008-07-11 | 2008-07-23 |
| 45 | n/a | Query | browser2 | http://inference-web.org/proofs/laptop/ex6.owl | 2007-11-14 | 2008-07-24 |
| 46 | cnf(add_equals_u_4,negated_conjecture,
( equalish(add(b,additive_inverse(a)),u) )).
cnf(less_or_equal_5,negated_conjecture,
( less_or_equal(additive_identity,u) )).
cnf(not_less_or_equal_6,negated_conjecture,
( ~ less_or_equal(a,b) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD068-2/query.owl | 2008-07-06 | 2008-07-23 |
| 47 | n/a | Query | browser2 | http://inference-web.org/proofs/tonys.moto.stanford.edu/tonys.owl | 2007-11-14 | 2008-07-24 |
| 48 | cnf(antecedent,negated_conjecture,
( ordered(x,y) )).
cnf(prove_wajsberg_theorem,negated_conjecture,
( ~ ordered(implies(x,z),implies(y,z)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/LCL/LCL142-1/query.owl | 2008-04-13 | 2008-07-23 |
| 49 | cnf(add_equals_c_4,negated_conjecture,
( equalish(add(a,b),c) )).
cnf(less_or_equal_5,negated_conjecture,
( less_or_equal(additive_identity,a) )).
cnf(less_or_equal_6,negated_conjecture,
( less_or_equal(additive_identity,b) )).
cnf(not_less_or_equal_7,negated_conjecture,
( ~ less_or_equal(additive_identity,c) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD070-2/query.owl | 2008-07-06 | 2008-07-23 |
| 50 | cnf(associativity_or_center,negated_conjecture,
( commutator(commutator(a,b),c) = commutator(a,commutator(b,c))
| multiply(commutator(e,f),g) = multiply(g,commutator(e,f)) )).
cnf(not_both_associativity_and_center,negated_conjecture,
( commutator(commutator(a,b),c) != commutator(a,commutator(b,c))
| multiply(commutator(e,f),g) != multiply(g,commutator(e,f)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/GRP/GRP024-4/query.owl | 2008-07-08 | 2008-07-23 |
| 51 | cnf(ap_reduce1_2c1,negated_conjecture,
( ~ member(pair(comb_app(p,r),comb_app(z,r)),rtrancl(contract)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/COL/COL088-1/query.owl | 2008-07-07 | 2008-07-23 |
| 52 | n/a | Query | browser2 | http://inference-web.org/proofs/wines/pastacolor.owl | 2007-11-14 | 2008-07-24 |
| 53 | n/a | Query | browser2 | http://inference-web.org/proofs/wines/blandfishwines.owl | 2007-11-14 | 2008-07-24 |
| 54 | cnf(a_not_equal_to_additive_identity_2,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(multiplicative_inverses_equal,negated_conjecture,
( equalish(multiplicative_inverse(a),multiplicative_identity) )).
cnf(a_not_equal_to_multiplicative_identity_4,negated_conjecture,
( ~ equalish(a,multiplicative_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD032-1/query.owl | 2008-07-06 | 2008-07-23 |
| 55 | cnf(a_not_equal_to_additive_identity_1,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(multiplicative_identity_equals_additive_identity_3,negated_conjecture,
( equalish(multiplicative_identity,additive_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD039-1/query.owl | 2008-07-06 | 2008-07-23 |
| 56 | cnf(a_not_equal_to_additive_identity_2,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(less_or_equal_3,negated_conjecture,
( less_or_equal(multiplicative_identity,a) )).
cnf(not_less_or_equal_4,negated_conjecture,
( ~ less_or_equal(multiplicative_inverse(a),multiplicative_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD091-1/query.owl | 2008-07-06 | 2008-07-23 |
| 57 | cnf(a_times_b_is_c,negated_conjecture,
( product(a,b,c) )).
cnf(c_times_inverse_a_is_d,negated_conjecture,
( product(c,inverse(a),d) )).
cnf(d_times_inverse_b_is_h,negated_conjecture,
( product(d,inverse(b),h) )).
cnf(h_times_b_is_j,negated_conjecture,
( product(h,b,j) )).
cnf(j_times_inverse_h_is_k,negated_conjecture,
( product(j,inverse(h),k) )).
cnf(prove_k_times_inverse_b_is_e,negated_conjecture,
( ~ product(k,inverse(b),identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/GRP/GRP002-1/query.owl | 2008-07-08 | 2008-07-23 |
| 58 | cnf(a_equals_multiplicative_identity_2,negated_conjecture,
( equalish(a,multiplicative_identity) )).
cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(multiplicative_inverses_not_equal,negated_conjecture,
( ~ equalish(multiplicative_inverse(a),multiplicative_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD031-1/query.owl | 2008-07-06 | 2008-07-23 |
| 59 | cnf(a_times_b_is_c,negated_conjecture,
( multiply(a,b) = c )).
cnf(prove_commutativity,negated_conjecture,
( multiply(b,a) != c )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/RNG/RNG008-4/query.owl | 2008-07-11 | 2008-07-23 |
| 60 | cnf(a_deciding_algorithm,negated_conjecture,
( algorithm(c4) )).
cnf(prove_the_algorithm_doesnt_exist,negated_conjecture,
( ~ program(Y1)
| decides(c4,Y1,Z1) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/COM/COM003-1/query.owl | 2008-07-07 | 2008-07-23 |
| 61 | cnf(a_not_equal_to_additive_identity_5,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(multiply_equals_b_6,negated_conjecture,
( equalish(multiply(a,u),b) )).
cnf(multiply_equals_b_7,negated_conjecture,
( equalish(multiply(a,v),b) )).
cnf(u_not_equal_to_v_8,negated_conjecture,
( ~ equalish(u,v) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD028-1/query.owl | 2008-07-06 | 2008-07-23 |
| 62 | cnf(a_times_b_is_c,negated_conjecture,
( multiply(a,b) = c )).
cnf(prove_commutativity,negated_conjecture,
( multiply(b,a) != c )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/RNG/RNG009-7/query.owl | 2008-07-11 | 2008-07-23 |
| 63 | cnf(an_3,negated_conjecture,
( ~ is_a_theorem(or(not(a),or(b,a))) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/LCL/LCL004-1/query.owl | 2008-04-13 | 2008-07-23 |
| 64 | cnf(add_equals_c_5,negated_conjecture,
( equalish(add(a,b),c) )).
cnf(add_equals_d_6,negated_conjecture,
( equalish(add(additive_inverse(a),additive_inverse(b)),d) )).
cnf(additive_inverse_not_equal_to_d_7,negated_conjecture,
( ~ equalish(additive_inverse(c),d) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD008-2/query.owl | 2008-07-06 | 2008-07-23 |
| 65 | cnf(ap_reduce1_2c1,negated_conjecture,
( ~ member(pair(comb_app(p,r),comb_app(z,r)),rtrancl(contract)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/COL/COL088-2/query.owl | 2008-07-07 | 2008-07-23 |
| 66 | n/a | Query | browser2 | http://inference-web.org/proofs/laptop/ex9.owl | 2007-11-14 | 2008-07-24 |
| 67 | cnf(a_not_additive_identity,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(prove_b_is_additive_identity,negated_conjecture,
( ~ equalish(b,additive_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/RNG/RNG038-2/query.owl | 2008-07-11 | 2008-07-23 |
| 68 | cnf(a_not_equal_to_additive_identity_2,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(less_or_equal_3,negated_conjecture,
( less_or_equal(multiplicative_identity,multiplicative_inverse(a)) )).
cnf(not_less_or_equal_4,negated_conjecture,
( ~ less_or_equal(a,multiplicative_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD093-1/query.owl | 2008-07-06 | 2008-07-23 |
| 69 | cnf(a_not_equal_to_additive_identity_2,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(multiplicative_inverse_not_equal_to_a_3,negated_conjecture,
( ~ equalish(multiplicative_inverse(multiplicative_inverse(a)),a) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD011-1/query.owl | 2008-07-06 | 2008-07-23 |
| 70 | cnf(assumption_2_37,negated_conjecture,
( organization(sk1) )).
cnf(assumption_2_38,negated_conjecture,
( has_immunity(sk1,sk2) )).
cnf(assumption_2_39,negated_conjecture,
( has_immunity(sk1,sk3) )).
cnf(assumption_2_40,negated_conjecture,
( hazard_of_mortality(sk1,sk2) != hazard_of_mortality(sk1,sk3) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/MGT/MGT059-1/query.owl | 2008-07-06 | 2008-07-24 |
| 71 | (type TonysSpecialty ?x) | Query | browser2 , browse | http://inference-web.org/proofs/primer/examples/tonys/query.owl | 2007-10-02 | 2008-07-24 |
| 72 | cnf(a_times_b_is_c,negated_conjecture,
( multiply(a,b) = c )).
cnf(prove_commutativity,negated_conjecture,
( multiply(b,a) != c )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/RNG/RNG008-3/query.owl | 2008-07-11 | 2008-07-23 |
| 73 | cnf(a_times_b_is_c,negated_conjecture,
( multiply(a,b) = c )).
cnf(prove_commutativity,negated_conjecture,
( multiply(b,a) != c )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/RNG/RNG035-7/query.owl | 2008-07-11 | 2008-07-23 |
| 74 | cnf(a_equals_additive_identity_2,negated_conjecture,
( equalish(a,additive_identity) )).
cnf(additive_inverse_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(additive_inverse(a),additive_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD018-1/query.owl | 2008-07-06 | 2008-07-23 |
| 75 | cnf(an_2,negated_conjecture,
( ~ is_a_theorem(or(not(or(a,b)),or(b,a))) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/LCL/LCL003-1/query.owl | 2008-04-13 | 2008-07-23 |
| 76 | cnf(a_times_b_is_c,negated_conjecture,
( multiply(a,b) = c )).
cnf(c_times_inverse_a_is_d,negated_conjecture,
( multiply(c,inverse(a)) = d )).
cnf(d_times_inverse_b_is_h,negated_conjecture,
( multiply(d,inverse(b)) = h )).
cnf(h_times_b_is_j,negated_conjecture,
( multiply(h,b) = j )).
cnf(j_times_inverse_h_is_k,negated_conjecture,
( multiply(j,inverse(h)) = k )).
cnf(prove_k_times_inverse_b_is_e,negated_conjecture,
( multiply(k,inverse(b)) != identity )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/GRP/GRP002-2/query.owl | 2008-07-08 | 2008-07-23 |
| 77 | cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(multiply_not_equal_to_b_4,negated_conjecture,
( ~ equalish(multiply(a,X),b) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD009-1/query.owl | 2008-07-06 | 2008-07-23 |
| 78 | cnf(ap_reduce2_2c1,negated_conjecture,
( ~ member(pair(comb_app(r,p),comb_app(r,z)),rtrancl(contract)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/COL/COL089-1/query.owl | 2008-07-07 | 2008-07-23 |
| 79 | cnf(add_not_equal_to_b_3,negated_conjecture,
( ~ equalish(add(a,X),b) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD005-1/query.owl | 2008-07-06 | 2008-07-23 |
| 80 | n/a | Query | browser2 | http://inference-web.org/proofs/laptop/ex10.owl | 2007-11-14 | 2008-07-24 |
| 81 | cnf(a_not_equal_to_additive_identity_2,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(less_or_equal_3,negated_conjecture,
( less_or_equal(multiplicative_inverse(a),additive_identity) )).
cnf(not_less_or_equal_4,negated_conjecture,
( ~ less_or_equal(a,additive_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD089-1/query.owl | 2008-07-06 | 2008-07-23 |
| 82 | cnf(a_times_b_is_c,negated_conjecture,
( multiply(a,b) = c )).
cnf(prove_commutativity,negated_conjecture,
( multiply(b,a) != c )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/RNG/RNG008-7/query.owl | 2008-07-11 | 2008-07-23 |
| 83 | (|Holds| (|hasOffice| |Ramazi| ?where) ?when) | Query | browser2 , browse | http://inference-web.org/proofs/RamaziHasOffice/Ramazis_offices_allen_noframe.owl | 2008-07-22 | 2008-07-24 |
| 84 | cnf(a_not_equal_to_additive_identity_2,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(less_or_equal_3,negated_conjecture,
( less_or_equal(multiplicative_inverse(a),additive_inverse(multiplicative_identity)) )).
cnf(not_less_or_equal_4,negated_conjecture,
( ~ less_or_equal(additive_inverse(multiplicative_identity),a) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD094-1/query.owl | 2008-07-06 | 2008-07-23 |
| 85 | cnf(a_equals_b_7,negated_conjecture,
( equalish(a,b) )).
cnf(c_equals_d_8,negated_conjecture,
( equalish(c,d) )).
cnf(multiply_equals_u_9,negated_conjecture,
( equalish(multiply(a,c),u) )).
cnf(multiply_equals_v_10,negated_conjecture,
( equalish(multiply(d,b),v) )).
cnf(v_not_equal_to_u_11,negated_conjecture,
( ~ equalish(v,u) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD025-2/query.owl | 2008-07-06 | 2008-07-23 |
| 86 | cnf(add_equals_a_3,negated_conjecture,
( equalish(add(m,a),a) )).
cnf(m_not_equal_to_additive_identity_4,negated_conjecture,
( ~ equalish(m,additive_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD020-1/query.owl | 2008-07-06 | 2008-07-23 |
| 87 | cnf(an_1,negated_conjecture,
( ~ is_a_theorem(or(not(or(not(b),c)),or(not(or(a,b)),or(a,c)))) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/LCL/LCL002-1/query.owl | 2008-04-13 | 2008-07-23 |
| 88 | cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(b_not_equal_to_additive_identity_4,negated_conjecture,
( ~ equalish(b,additive_identity) )).
cnf(multiplicative_inverses_equal,negated_conjecture,
( equalish(multiplicative_inverse(a),multiplicative_inverse(b)) )).
cnf(a_not_equal_to_b_6,negated_conjecture,
( ~ equalish(a,b) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD027-1/query.owl | 2008-07-06 | 2008-07-23 |
| 89 | cnf(a_not_equal_to_additive_identity_4,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(b_not_equal_to_additive_identity_5,negated_conjecture,
( ~ equalish(b,additive_identity) )).
cnf(multiply_equals_c_6,negated_conjecture,
( equalish(multiply(a,b),c) )).
cnf(c_equals_additive_identity_7,negated_conjecture,
( equalish(c,additive_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD041-2/query.owl | 2008-07-06 | 2008-07-23 |
| 90 | cnf(ap_reduce2_2c1,negated_conjecture,
( ~ member(pair(comb_app(r,p),comb_app(r,z)),rtrancl(contract)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/COL/COL089-2/query.owl | 2008-07-07 | 2008-07-23 |
| 91 | cnf(additive_identity_equals_add_3,negated_conjecture,
( equalish(additive_identity,add(b,additive_inverse(a))) )).
cnf(a_not_equal_to_b_4,negated_conjecture,
( ~ equalish(a,b) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD024-1/query.owl | 2008-07-06 | 2008-07-23 |
| 92 | n/a | Query | browser2 | http://inference-web.org/proofs/tonys.orig/tonys.owl | 2007-11-14 | 2008-07-24 |
| 93 | cnf(a_not_equal_to_additive_identity_2,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(mult_inverse_not_equal_to_additive_inverse_3,negated_conjecture,
( ~ equalish(multiplicative_inverse(additive_inverse(a)),additive_inverse(multiplicative_inverse(a))) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD046-1/query.owl | 2008-07-06 | 2008-07-23 |
| 94 | (|http://www.w3.org/1999/02/22-rdf-syntax-ns#|::type |http://iw.stanford.edu/enginesdoc/jtp/script-data/tonys.daml#|::|TonysSpecialty| ?x) | Query | browser2 , browse | http://inference-web.org/proofs/tonys/tonys.owl | 2008-07-22 | 2008-07-24 |
| 95 | cnf(a_equals_d_4,negated_conjecture,
( equalish(a,d) )).
cnf(multiply_not_equal_to_multiply_5,negated_conjecture,
( ~ equalish(multiply(d,b),multiply(a,b)) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD030-1/query.owl | 2008-07-06 | 2008-07-23 |
| 96 | cnf(a_times_b_is_c,negated_conjecture,
( product(a,b,c) )).
cnf(prove_b_times_a_is_c,negated_conjecture,
( ~ product(b,a,c) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/GRP/GRP001-1/query.owl | 2008-07-08 | 2008-07-23 |
| 97 | cnf(additive_inverse_not_equal_to_additive_identity_1,negated_conjecture,
( ~ equalish(additive_inverse(additive_identity),additive_identity) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD006-1/query.owl | 2008-07-06 | 2008-07-23 |
| 98 | cnf(a_not_equal_to_additive_identity_3,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(b_not_equal_to_additive_identity_4,negated_conjecture,
( ~ equalish(b,additive_identity) )).
cnf(multiplicative_inverse_not_equal_to_multiply_5,negated_conjecture,
( ~ equalish(multiplicative_inverse(multiply(a,b)),multiply(multiplicative_inverse(a),multiplicative_inverse(b))) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD012-1/query.owl | 2008-07-06 | 2008-07-23 |
| 99 | cnf(a_not_equal_to_additive_identity_5,negated_conjecture,
( ~ equalish(a,additive_identity) )).
cnf(b_not_equal_to_additive_identity_6,negated_conjecture,
( ~ equalish(b,additive_identity) )).
cnf(multiply_equals_u_7,negated_conjecture,
( equalish(multiply(a,b),u) )).
cnf(multiply_equals_v_8,negated_conjecture,
( equalish(multiply(multiplicative_inverse(a),multiplicative_inverse(b)),v) )).
cnf(multiplicative_inverse_not_equal_to_v_9,negated_conjecture,
( ~ equalish(multiplicative_inverse(u),v) )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/FLD/FLD012-2/query.owl | 2008-07-06 | 2008-07-23 |
| 100 | cnf(a_times_b_is_c,negated_conjecture,
( multiply(a,b) = c )).
cnf(prove_commutativity,negated_conjecture,
( multiply(b,a) != c )). | Query | browser2 , browse | http://inference-web.org/proofs/tptp/Problems/RNG/RNG036-7/query.owl | 2008-07-11 | 2008-07-23 |