%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : REL029-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:33:55 PM UTC 2026
% Result : Unsatisfiable 13.27s 2.78s
% Output : Refutation 14.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 16
% Syntax : Number of formulae : 257 ( 257 unt; 0 def)
% Number of atoms : 257 ( 256 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 8 ( 8 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 361 ( 361 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux1_join_commutativity_1) ).
fof(f2,axiom,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux2_join_associativity_2) ).
fof(f3,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan_3) ).
fof(f4,plain,
! [X0,X1] : join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) = X0,
inference(reorient_equations,[],[f3]) ).
fof(f5,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux4_definiton_of_meet_4) ).
fof(f6,plain,
! [X0,X1] : complement(join(complement(X0),complement(X1))) = meet(X0,X1),
inference(reorient_equations,[],[f5]) ).
fof(f7,axiom,
! [X2,X0,X1] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_associativity_5) ).
fof(f8,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_identity_6) ).
fof(f9,axiom,
! [X2,X0,X1] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_distributivity_7) ).
fof(f10,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_idempotence_8) ).
fof(f11,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_additivity_9) ).
fof(f12,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_multiplicativity_10) ).
fof(f13,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_cancellativity_11) ).
fof(f14,plain,
! [X0,X1] : complement(X1) = join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)),
inference(reorient_equations,[],[f13]) ).
fof(f15,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_top_12) ).
fof(f16,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_zero_13) ).
fof(f17,negated_conjecture,
join(sk1,one) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_14) ).
fof(f18,plain,
one = join(sk1,one),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
join(sk2,one) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_15) ).
fof(f20,plain,
one = join(sk2,one),
inference(reorient_equations,[],[f19]) ).
fof(f21,negated_conjecture,
meet(composition(sk1,sk3),composition(sk2,sk3)) != composition(meet(sk1,sk2),sk3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_16) ).
fof(f22,plain,
complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) != composition(complement(join(complement(sk1),complement(sk2))),sk3),
inference(definition_unfolding,[],[f21,f6,f6]) ).
fof(f23,plain,
! [X0] : zero = complement(join(complement(X0),complement(complement(X0)))),
inference(definition_unfolding,[],[f16,f6]) ).
fof(f24,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f4,f1]) ).
fof(f25,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(converse(X0),complement(composition(X0,X1)))),
inference(forward_demodulation,[],[f14,f1]) ).
fof(f26,plain,
one = join(one,sk2),
inference(forward_demodulation,[],[f20,f1]) ).
fof(f27,plain,
one = join(one,sk1),
inference(forward_demodulation,[],[f18,f1]) ).
fof(f28,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(join(complement(X0),X1)),complement(complement(join(complement(X0),complement(X1))))))),
inference(superposition,[],[f24,f24]) ).
fof(f30,plain,
! [X0,X1] : join(complement(join(X0,complement(X1))),complement(join(complement(X1),complement(X0)))) = X1,
inference(superposition,[],[f24,f1]) ).
fof(f31,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(join(complement(join(complement(X0),X1)),join(complement(X0),complement(X1)))),complement(X0)),
inference(superposition,[],[f24,f24]) ).
fof(f33,plain,
! [X0,X1] : join(complement(join(complement(X1),X0)),complement(join(complement(X0),complement(X1)))) = X1,
inference(superposition,[],[f24,f1]) ).
fof(f34,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(join(complement(X0),X1)),join(complement(X0),complement(X1))))),
inference(forward_demodulation,[],[f31,f1]) ).
fof(f35,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(join(complement(X0),complement(X1)),complement(join(complement(X0),X1))))),
inference(forward_demodulation,[],[f34,f1]) ).
fof(f36,plain,
! [X0,X1] : join(complement(X0),X1) = join(complement(X0),complement(join(complement(X0),join(complement(X1),complement(join(complement(X0),X1)))))),
inference(forward_demodulation,[],[f35,f2]) ).
fof(f75,plain,
zero = complement(top),
inference(superposition,[],[f23,f15]) ).
fof(f107,plain,
! [X0,X1] : converse(join(converse(X0),X1)) = join(X0,converse(X1)),
inference(superposition,[],[f11,f10]) ).
fof(f114,plain,
! [X0,X1] : converse(composition(converse(X0),X1)) = composition(converse(X1),X0),
inference(superposition,[],[f12,f10]) ).
fof(f116,plain,
! [X2,X0,X1] : composition(join(converse(X1),X2),converse(X0)) = join(converse(composition(X0,X1)),composition(X2,converse(X0))),
inference(superposition,[],[f9,f12]) ).
fof(f120,plain,
! [X0] : converse(converse(X0)) = composition(converse(one),X0),
inference(superposition,[],[f114,f8]) ).
fof(f128,plain,
! [X0] : composition(converse(one),X0) = X0,
inference(forward_demodulation,[],[f120,f10]) ).
fof(f138,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = join(converse(composition(X0,X2)),converse(composition(X0,X1))),
inference(superposition,[],[f116,f12]) ).
fof(f143,plain,
! [X2,X0,X1] : composition(join(converse(X2),converse(X1)),converse(X0)) = converse(join(composition(X0,X2),composition(X0,X1))),
inference(forward_demodulation,[],[f138,f11]) ).
fof(f148,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = composition(converse(join(X2,X1)),converse(X0)),
inference(forward_demodulation,[],[f143,f11]) ).
fof(f151,plain,
! [X2,X0,X1] : converse(join(composition(X0,X2),composition(X0,X1))) = converse(composition(X0,join(X2,X1))),
inference(forward_demodulation,[],[f148,f12]) ).
fof(f227,plain,
! [X0,X1] : join(X0,join(complement(X0),X1)) = join(top,X1),
inference(superposition,[],[f2,f15]) ).
fof(f229,plain,
! [X2,X0,X1] : join(X0,X2) = join(complement(join(complement(X0),X1)),join(complement(join(complement(X0),complement(X1))),X2)),
inference(superposition,[],[f2,f24]) ).
fof(f242,plain,
! [X2,X0,X1] : join(X0,join(X1,X2)) = join(X2,join(X0,X1)),
inference(superposition,[],[f1,f2]) ).
fof(f269,plain,
! [X0,X1] : join(X1,complement(join(complement(X0),complement(complement(X1))))) = join(complement(join(complement(X1),X0)),X0),
inference(superposition,[],[f229,f30]) ).
fof(f287,plain,
! [X0,X1] : join(X1,complement(join(complement(X0),complement(complement(X1))))) = join(X0,complement(join(complement(X1),X0))),
inference(forward_demodulation,[],[f269,f1]) ).
fof(f412,plain,
! [X0,X1] : complement(X1) = join(complement(X1),composition(X0,complement(composition(converse(X0),X1)))),
inference(superposition,[],[f25,f10]) ).
fof(f491,plain,
! [X2,X0,X1] : join(composition(X0,X1),composition(X0,X2)) = converse(converse(composition(X0,join(X1,X2)))),
inference(superposition,[],[f10,f151]) ).
fof(f504,plain,
! [X2,X0,X1] : composition(X0,join(X1,X2)) = join(composition(X0,X1),composition(X0,X2)),
inference(forward_demodulation,[],[f491,f10]) ).
fof(f517,plain,
! [X0,X1] : composition(X0,join(one,X1)) = join(X0,composition(X0,X1)),
inference(superposition,[],[f504,f8]) ).
fof(f531,plain,
! [X0] : composition(X0,one) = join(X0,composition(X0,sk1)),
inference(superposition,[],[f517,f27]) ).
fof(f532,plain,
! [X0] : composition(X0,one) = join(X0,composition(X0,sk2)),
inference(superposition,[],[f517,f26]) ).
fof(f577,plain,
! [X0] : join(X0,composition(X0,sk2)) = X0,
inference(forward_demodulation,[],[f532,f8]) ).
fof(f578,plain,
! [X0] : join(X0,composition(X0,sk1)) = X0,
inference(forward_demodulation,[],[f531,f8]) ).
fof(f701,plain,
one = converse(one),
inference(superposition,[],[f8,f128]) ).
fof(f746,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(composition(converse(X0),sk1))),
inference(superposition,[],[f107,f578]) ).
fof(f747,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(composition(converse(X0),sk2))),
inference(superposition,[],[f107,f577]) ).
fof(f758,plain,
! [X0] : converse(converse(X0)) = join(X0,composition(converse(sk2),X0)),
inference(forward_demodulation,[],[f747,f114]) ).
fof(f759,plain,
! [X0] : converse(converse(X0)) = join(X0,composition(converse(sk1),X0)),
inference(forward_demodulation,[],[f746,f114]) ).
fof(f766,plain,
! [X0] : join(X0,composition(converse(sk2),X0)) = X0,
inference(forward_demodulation,[],[f758,f10]) ).
fof(f767,plain,
! [X0] : join(X0,composition(converse(sk1),X0)) = X0,
inference(forward_demodulation,[],[f759,f10]) ).
fof(f793,plain,
! [X0] : composition(X0,one) = join(X0,composition(X0,composition(converse(sk1),one))),
inference(superposition,[],[f517,f767]) ).
fof(f796,plain,
! [X0] : composition(X0,one) = join(X0,composition(X0,converse(sk1))),
inference(forward_demodulation,[],[f793,f8]) ).
fof(f807,plain,
! [X0] : join(X0,composition(X0,converse(sk1))) = X0,
inference(forward_demodulation,[],[f796,f8]) ).
fof(f830,plain,
! [X0] : composition(X0,one) = join(X0,composition(X0,composition(converse(sk2),one))),
inference(superposition,[],[f517,f766]) ).
fof(f833,plain,
! [X0] : composition(X0,one) = join(X0,composition(X0,converse(sk2))),
inference(forward_demodulation,[],[f830,f8]) ).
fof(f844,plain,
! [X0] : join(X0,composition(X0,converse(sk2))) = X0,
inference(forward_demodulation,[],[f833,f8]) ).
fof(f870,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(composition(converse(X0),converse(sk1)))),
inference(superposition,[],[f107,f807]) ).
fof(f871,plain,
! [X0] : converse(converse(X0)) = join(X0,composition(converse(converse(sk1)),X0)),
inference(forward_demodulation,[],[f870,f114]) ).
fof(f889,plain,
! [X0] : converse(converse(X0)) = join(X0,composition(sk1,X0)),
inference(forward_demodulation,[],[f871,f10]) ).
fof(f897,plain,
! [X0] : join(X0,composition(sk1,X0)) = X0,
inference(forward_demodulation,[],[f889,f10]) ).
fof(f904,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(composition(sk1,X0),X1)),
inference(superposition,[],[f2,f897]) ).
fof(f930,plain,
! [X0,X1] : join(X0,composition(sk1,X1)) = join(X0,composition(sk1,join(X0,X1))),
inference(superposition,[],[f904,f504]) ).
fof(f1015,plain,
! [X0] : converse(converse(X0)) = join(X0,converse(composition(converse(X0),converse(sk2)))),
inference(superposition,[],[f107,f844]) ).
fof(f1016,plain,
! [X0] : converse(converse(X0)) = join(X0,composition(converse(converse(sk2)),X0)),
inference(forward_demodulation,[],[f1015,f114]) ).
fof(f1035,plain,
! [X0] : converse(converse(X0)) = join(X0,composition(sk2,X0)),
inference(forward_demodulation,[],[f1016,f10]) ).
fof(f1044,plain,
! [X0] : join(X0,composition(sk2,X0)) = X0,
inference(forward_demodulation,[],[f1035,f10]) ).
fof(f1049,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(composition(sk2,X0),X1)),
inference(superposition,[],[f242,f1044]) ).
fof(f1051,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(composition(sk2,X0),X1)),
inference(superposition,[],[f2,f1044]) ).
fof(f1079,plain,
! [X0,X1] : join(X0,composition(sk2,X1)) = join(X0,composition(sk2,join(X0,X1))),
inference(superposition,[],[f1051,f504]) ).
fof(f1158,plain,
! [X0] : join(X0,composition(sk1,complement(X0))) = join(X0,composition(sk1,top)),
inference(superposition,[],[f930,f15]) ).
fof(f1294,plain,
! [X0] : join(X0,composition(sk2,complement(X0))) = join(X0,composition(sk2,top)),
inference(superposition,[],[f1079,f15]) ).
fof(f2502,plain,
! [X0] : composition(one,X0) = X0,
inference(superposition,[],[f128,f701]) ).
fof(f2532,plain,
! [X0] : complement(X0) = join(complement(X0),complement(composition(converse(one),X0))),
inference(superposition,[],[f412,f2502]) ).
fof(f2539,plain,
! [X0] : complement(X0) = join(complement(X0),complement(X0)),
inference(forward_demodulation,[],[f2532,f128]) ).
fof(f2558,plain,
! [X0] : join(X0,complement(X0)) = join(top,complement(X0)),
inference(superposition,[],[f227,f2539]) ).
fof(f2563,plain,
! [X0,X1] : join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))) = join(X0,complement(join(complement(X0),complement(X1)))),
inference(superposition,[],[f229,f2539]) ).
fof(f2564,plain,
! [X0] : join(complement(complement(X0)),complement(join(complement(X0),complement(complement(X0))))) = X0,
inference(superposition,[],[f30,f2539]) ).
fof(f2572,plain,
! [X0] : join(X0,complement(join(complement(complement(complement(X0))),complement(complement(X0))))) = X0,
inference(forward_demodulation,[],[f2564,f287]) ).
fof(f2573,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),complement(X1)))) = X0,
inference(forward_demodulation,[],[f2563,f24]) ).
fof(f2578,plain,
! [X0] : top = join(top,complement(X0)),
inference(forward_demodulation,[],[f2558,f15]) ).
fof(f2583,plain,
! [X0] : join(X0,complement(join(complement(complement(X0)),complement(complement(complement(X0)))))) = X0,
inference(forward_demodulation,[],[f2572,f1]) ).
fof(f2592,plain,
! [X0] : join(X0,zero) = X0,
inference(forward_demodulation,[],[f2583,f23]) ).
fof(f2612,plain,
! [X0] : join(zero,X0) = X0,
inference(superposition,[],[f1,f2592]) ).
fof(f2656,plain,
! [X0] : join(complement(top),complement(join(complement(X0),complement(top)))) = X0,
inference(superposition,[],[f30,f2578]) ).
fof(f2671,plain,
! [X0] : join(zero,complement(join(complement(X0),zero))) = X0,
inference(forward_demodulation,[],[f2656,f75]) ).
fof(f2674,plain,
! [X0] : complement(join(complement(X0),zero)) = X0,
inference(forward_demodulation,[],[f2671,f2612]) ).
fof(f2675,plain,
! [X0] : complement(join(zero,complement(X0))) = X0,
inference(forward_demodulation,[],[f2674,f1]) ).
fof(f2676,plain,
! [X0] : complement(complement(X0)) = X0,
inference(forward_demodulation,[],[f2675,f2612]) ).
fof(f2682,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(X0,complement(X1)))),
inference(superposition,[],[f24,f2676]) ).
fof(f2688,plain,
! [X0,X1] : complement(X0) = join(complement(join(X0,X1)),complement(join(complement(X1),X0))),
inference(superposition,[],[f33,f2676]) ).
fof(f2695,plain,
! [X0] : join(complement(X0),composition(sk1,top)) = join(complement(X0),composition(sk1,X0)),
inference(superposition,[],[f1158,f2676]) ).
fof(f2696,plain,
! [X0] : join(complement(X0),composition(sk2,top)) = join(complement(X0),composition(sk2,X0)),
inference(superposition,[],[f1294,f2676]) ).
fof(f2697,plain,
! [X0] : join(X0,X0) = X0,
inference(superposition,[],[f2539,f2676]) ).
fof(f2698,plain,
! [X0] : top = join(top,X0),
inference(superposition,[],[f2578,f2676]) ).
fof(f2932,plain,
! [X0,X1] : join(X1,X0) = join(X0,join(X0,X1)),
inference(superposition,[],[f242,f2697]) ).
fof(f3399,plain,
! [X0,X1] : join(X0,complement(join(complement(X0),X1))) = X0,
inference(superposition,[],[f2573,f36]) ).
fof(f3400,plain,
! [X0,X1] : join(X0,X1) = join(join(X0,X1),complement(complement(X0))),
inference(superposition,[],[f2573,f2682]) ).
fof(f3473,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,complement(complement(X0)))),
inference(forward_demodulation,[],[f3400,f2]) ).
fof(f3496,plain,
! [X0,X1] : join(X0,X1) = join(X0,join(X1,X0)),
inference(forward_demodulation,[],[f3473,f2676]) ).
fof(f3536,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X0,X1))),
inference(superposition,[],[f3399,f2676]) ).
fof(f3555,plain,
! [X0,X1] : join(X1,complement(join(X0,complement(X1)))) = X1,
inference(superposition,[],[f3399,f1049]) ).
fof(f3701,plain,
! [X0,X1] : complement(X0) = join(complement(X0),complement(join(X1,X0))),
inference(superposition,[],[f3555,f2676]) ).
fof(f3850,plain,
! [X0] : complement(composition(sk1,X0)) = join(complement(composition(sk1,X0)),complement(X0)),
inference(superposition,[],[f3701,f897]) ).
fof(f3854,plain,
! [X0] : complement(composition(sk2,X0)) = join(complement(composition(sk2,X0)),complement(X0)),
inference(superposition,[],[f3701,f1044]) ).
fof(f3874,plain,
complement(sk2) = join(complement(sk2),complement(one)),
inference(superposition,[],[f3701,f26]) ).
fof(f3926,plain,
complement(sk2) = join(complement(one),complement(sk2)),
inference(forward_demodulation,[],[f3874,f1]) ).
fof(f3941,plain,
! [X0] : complement(composition(sk2,X0)) = join(complement(X0),complement(composition(sk2,X0))),
inference(forward_demodulation,[],[f3854,f1]) ).
fof(f3944,plain,
! [X0] : complement(composition(sk1,X0)) = join(complement(X0),complement(composition(sk1,X0))),
inference(forward_demodulation,[],[f3850,f1]) ).
fof(f5100,plain,
! [X2,X0,X1] : complement(X1) = join(complement(X1),complement(join(X0,join(X1,X2)))),
inference(superposition,[],[f3536,f242]) ).
fof(f7317,plain,
! [X0,X1] : complement(join(complement(complement(X1)),X0)) = join(complement(join(join(complement(complement(X1)),X0),X1)),complement(join(top,X0))),
inference(superposition,[],[f2688,f227]) ).
fof(f7356,plain,
! [X0,X1] : join(complement(join(X0,X1)),join(complement(X1),X0)) = join(complement(join(X0,X1)),complement(join(complement(join(complement(join(X0,X1)),join(complement(X1),X0))),complement(complement(complement(X0)))))),
inference(superposition,[],[f28,f2688]) ).
fof(f7372,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(complement(join(complement(X1),X0)),complement(complement(join(X0,X1)))))),
inference(superposition,[],[f30,f2688]) ).
fof(f7393,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(complement(join(complement(X1),X0)),join(X0,X1)))),
inference(forward_demodulation,[],[f7372,f2676]) ).
fof(f7409,plain,
! [X0,X1] : join(complement(join(X0,X1)),join(complement(X1),X0)) = join(complement(join(X0,X1)),complement(join(complement(complement(complement(X0))),complement(join(complement(join(X0,X1)),join(complement(X1),X0)))))),
inference(forward_demodulation,[],[f7356,f1]) ).
fof(f7444,plain,
! [X0,X1] : complement(join(complement(complement(X1)),X0)) = join(complement(join(top,X0)),complement(join(join(complement(complement(X1)),X0),X1))),
inference(forward_demodulation,[],[f7317,f1]) ).
fof(f7526,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(join(X0,X1),complement(join(complement(X1),X0))))),
inference(forward_demodulation,[],[f7393,f1]) ).
fof(f7542,plain,
! [X0,X1] : join(join(complement(X1),X0),complement(join(X0,X1))) = join(complement(join(X0,X1)),complement(join(complement(complement(complement(X0))),complement(join(join(complement(X1),X0),complement(join(X0,X1))))))),
inference(forward_demodulation,[],[f7409,f1]) ).
fof(f7572,plain,
! [X0,X1] : complement(join(complement(complement(X1)),X0)) = join(complement(join(top,X0)),complement(join(X1,join(complement(complement(X1)),X0)))),
inference(forward_demodulation,[],[f7444,f1]) ).
fof(f7629,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(X0,join(X1,complement(join(complement(X1),X0)))))),
inference(forward_demodulation,[],[f7526,f2]) ).
fof(f7644,plain,
! [X0,X1] : join(complement(X1),join(X0,complement(join(X0,X1)))) = join(complement(join(X0,X1)),complement(join(complement(complement(complement(X0))),complement(join(complement(X1),join(X0,complement(join(X0,X1)))))))),
inference(forward_demodulation,[],[f7542,f2]) ).
fof(f7673,plain,
! [X0,X1] : complement(join(X1,X0)) = join(complement(join(top,X0)),complement(join(X1,join(X1,X0)))),
inference(forward_demodulation,[],[f7572,f2676]) ).
fof(f7717,plain,
! [X0,X1] : join(complement(X1),X0) = join(complement(complement(X0)),complement(join(X0,X1))),
inference(forward_demodulation,[],[f7629,f3399]) ).
fof(f7727,plain,
! [X0,X1] : join(complement(X1),join(X0,complement(join(X0,X1)))) = join(complement(join(X0,X1)),complement(join(complement(X0),complement(join(complement(X1),join(X0,complement(join(X0,X1)))))))),
inference(forward_demodulation,[],[f7644,f2676]) ).
fof(f7745,plain,
! [X0,X1] : complement(join(X1,X0)) = join(complement(join(top,X0)),complement(join(X0,X1))),
inference(forward_demodulation,[],[f7673,f2932]) ).
fof(f7779,plain,
! [X0,X1] : join(complement(X1),X0) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f7717,f2676]) ).
fof(f7787,plain,
! [X0,X1] : join(complement(X1),join(X0,complement(join(X0,X1)))) = join(complement(join(X0,X1)),complement(complement(X0))),
inference(forward_demodulation,[],[f7727,f5100]) ).
fof(f7799,plain,
! [X0,X1] : complement(join(X1,X0)) = join(complement(top),complement(join(X0,X1))),
inference(forward_demodulation,[],[f7745,f2698]) ).
fof(f7818,plain,
! [X0,X1] : join(complement(complement(X0)),complement(join(X0,X1))) = join(complement(X1),join(X0,complement(join(X0,X1)))),
inference(forward_demodulation,[],[f7787,f1]) ).
fof(f7821,plain,
! [X0,X1] : complement(join(X1,X0)) = join(zero,complement(join(X0,X1))),
inference(forward_demodulation,[],[f7799,f75]) ).
fof(f7835,plain,
! [X0,X1] : join(complement(complement(X0)),complement(join(X0,X1))) = join(complement(X1),join(complement(X1),X0)),
inference(forward_demodulation,[],[f7818,f7779]) ).
fof(f7838,plain,
! [X0,X1] : complement(join(X0,X1)) = complement(join(X1,X0)),
inference(forward_demodulation,[],[f7821,f2612]) ).
fof(f7844,plain,
! [X0,X1] : join(X0,complement(X1)) = join(complement(complement(X0)),complement(join(X0,X1))),
inference(forward_demodulation,[],[f7835,f2932]) ).
fof(f7848,plain,
! [X0,X1] : join(X0,complement(X1)) = join(X0,complement(join(X0,X1))),
inference(forward_demodulation,[],[f7844,f2676]) ).
fof(f7913,plain,
! [X0] : join(complement(composition(sk1,top)),complement(X0)) = join(complement(X0),complement(join(complement(X0),composition(sk1,X0)))),
inference(superposition,[],[f7779,f2695]) ).
fof(f7914,plain,
! [X0] : join(complement(composition(sk2,top)),complement(X0)) = join(complement(X0),complement(join(complement(X0),composition(sk2,X0)))),
inference(superposition,[],[f7779,f2696]) ).
fof(f8044,plain,
! [X0] : join(complement(composition(sk2,X0)),complement(X0)) = join(complement(composition(sk2,top)),complement(X0)),
inference(forward_demodulation,[],[f7914,f7779]) ).
fof(f8045,plain,
! [X0] : join(complement(composition(sk1,X0)),complement(X0)) = join(complement(composition(sk1,top)),complement(X0)),
inference(forward_demodulation,[],[f7913,f7779]) ).
fof(f8133,plain,
! [X0] : join(complement(X0),complement(composition(sk2,X0))) = join(complement(composition(sk2,top)),complement(X0)),
inference(forward_demodulation,[],[f8044,f1]) ).
fof(f8134,plain,
! [X0] : join(complement(X0),complement(composition(sk1,X0))) = join(complement(composition(sk1,top)),complement(X0)),
inference(forward_demodulation,[],[f8045,f1]) ).
fof(f8205,plain,
! [X0] : complement(composition(sk2,X0)) = join(complement(composition(sk2,top)),complement(X0)),
inference(forward_demodulation,[],[f8133,f3941]) ).
fof(f8206,plain,
! [X0] : complement(composition(sk1,X0)) = join(complement(composition(sk1,top)),complement(X0)),
inference(forward_demodulation,[],[f8134,f3944]) ).
fof(f8352,plain,
! [X0] : join(complement(X0),complement(composition(sk1,top))) = join(complement(X0),complement(join(complement(X0),composition(sk1,X0)))),
inference(superposition,[],[f7848,f2695]) ).
fof(f8353,plain,
! [X0] : join(complement(X0),complement(composition(sk2,top))) = join(complement(X0),complement(join(complement(X0),composition(sk2,X0)))),
inference(superposition,[],[f7848,f2696]) ).
fof(f8481,plain,
! [X0] : join(complement(composition(sk2,X0)),complement(X0)) = join(complement(X0),complement(composition(sk2,top))),
inference(forward_demodulation,[],[f8353,f7779]) ).
fof(f8482,plain,
! [X0] : join(complement(composition(sk1,X0)),complement(X0)) = join(complement(X0),complement(composition(sk1,top))),
inference(forward_demodulation,[],[f8352,f7779]) ).
fof(f8564,plain,
! [X0] : join(complement(X0),complement(composition(sk2,X0))) = join(complement(X0),complement(composition(sk2,top))),
inference(forward_demodulation,[],[f8481,f1]) ).
fof(f8565,plain,
! [X0] : join(complement(X0),complement(composition(sk1,X0))) = join(complement(X0),complement(composition(sk1,top))),
inference(forward_demodulation,[],[f8482,f1]) ).
fof(f8615,plain,
! [X0] : complement(composition(sk2,X0)) = join(complement(X0),complement(composition(sk2,top))),
inference(forward_demodulation,[],[f8564,f3941]) ).
fof(f8616,plain,
! [X0] : complement(composition(sk1,X0)) = join(complement(X0),complement(composition(sk1,top))),
inference(forward_demodulation,[],[f8565,f3944]) ).
fof(f10238,plain,
! [X0] : complement(composition(sk1,complement(X0))) = join(complement(composition(sk1,top)),X0),
inference(superposition,[],[f8206,f2676]) ).
fof(f10526,plain,
! [X0] : complement(composition(sk2,complement(X0))) = join(complement(composition(sk2,top)),X0),
inference(superposition,[],[f8205,f2676]) ).
fof(f10849,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = join(complement(X0),join(complement(composition(sk1,top)),X1)),
inference(superposition,[],[f242,f8616]) ).
fof(f10850,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = join(complement(composition(sk1,top)),join(X1,complement(X0))),
inference(superposition,[],[f242,f8616]) ).
fof(f10862,plain,
! [X0] : join(complement(composition(sk1,top)),complement(X0)) = join(complement(composition(sk1,top)),complement(composition(sk1,X0))),
inference(superposition,[],[f3496,f8616]) ).
fof(f10877,plain,
! [X0] : complement(composition(sk1,composition(sk1,X0))) = join(complement(composition(sk1,top)),complement(X0)),
inference(forward_demodulation,[],[f10862,f8206]) ).
fof(f10883,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = complement(composition(sk1,complement(join(X1,complement(X0))))),
inference(forward_demodulation,[],[f10850,f10238]) ).
fof(f10884,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = join(complement(X0),complement(composition(sk1,complement(X1)))),
inference(forward_demodulation,[],[f10849,f10238]) ).
fof(f10917,plain,
! [X0] : complement(composition(sk1,X0)) = complement(composition(sk1,composition(sk1,X0))),
inference(forward_demodulation,[],[f10877,f8206]) ).
fof(f10978,plain,
! [X0,X1] : join(X1,complement(composition(sk1,complement(X0)))) = complement(composition(sk1,complement(join(X1,X0)))),
inference(superposition,[],[f10883,f2676]) ).
fof(f11003,plain,
! [X0] : join(complement(composition(sk2,top)),complement(composition(sk1,X0))) = complement(composition(sk1,complement(complement(composition(sk2,X0))))),
inference(superposition,[],[f10883,f8205]) ).
fof(f11015,plain,
! [X0] : complement(composition(sk1,complement(complement(composition(sk2,X0))))) = join(complement(X0),complement(composition(sk1,composition(sk2,X0)))),
inference(superposition,[],[f10883,f3941]) ).
fof(f11027,plain,
! [X0,X1] : join(X1,complement(composition(sk1,X0))) = complement(composition(sk1,complement(join(complement(X0),X1)))),
inference(superposition,[],[f10883,f7838]) ).
fof(f11127,plain,
! [X0] : complement(composition(sk1,composition(sk2,X0))) = join(complement(X0),complement(composition(sk1,composition(sk2,X0)))),
inference(forward_demodulation,[],[f11015,f2676]) ).
fof(f11136,plain,
! [X0] : complement(composition(sk1,composition(sk2,X0))) = join(complement(composition(sk2,top)),complement(composition(sk1,X0))),
inference(forward_demodulation,[],[f11003,f2676]) ).
fof(f11198,plain,
! [X0] : complement(composition(sk1,composition(sk2,X0))) = complement(composition(sk2,composition(sk1,X0))),
inference(forward_demodulation,[],[f11136,f8205]) ).
fof(f11280,plain,
! [X0,X1] : complement(composition(sk1,complement(join(X0,X1)))) = join(X1,complement(composition(sk1,complement(X0)))),
inference(superposition,[],[f11027,f2676]) ).
fof(f11360,plain,
! [X0,X1] : join(complement(X0),complement(composition(sk1,X1))) = join(complement(X1),complement(composition(sk1,X0))),
inference(superposition,[],[f10883,f11027]) ).
fof(f11407,plain,
! [X0,X1] : join(complement(composition(sk2,top)),join(X0,complement(composition(sk1,X1)))) = complement(composition(sk2,composition(sk1,complement(join(complement(X1),X0))))),
inference(superposition,[],[f8205,f11027]) ).
fof(f11414,plain,
! [X0,X1] : join(complement(composition(sk2,top)),join(X0,complement(composition(sk1,X1)))) = complement(composition(sk1,composition(sk2,complement(join(complement(X1),X0))))),
inference(forward_demodulation,[],[f11407,f11198]) ).
fof(f11532,plain,
! [X0,X1] : complement(composition(sk2,complement(join(X0,complement(composition(sk1,X1)))))) = complement(composition(sk1,composition(sk2,complement(join(complement(X1),X0))))),
inference(forward_demodulation,[],[f11414,f10526]) ).
fof(f12215,plain,
! [X2,X0,X1] : join(join(X0,X1),complement(composition(sk1,X2))) = join(complement(X2),join(X0,complement(composition(sk1,complement(X1))))),
inference(superposition,[],[f10884,f10978]) ).
fof(f12238,plain,
! [X0] : complement(composition(sk2,composition(sk1,complement(X0)))) = join(X0,complement(composition(sk1,composition(sk2,top)))),
inference(superposition,[],[f8205,f10884]) ).
fof(f12314,plain,
! [X0] : complement(composition(sk1,composition(sk2,complement(X0)))) = join(X0,complement(composition(sk1,composition(sk2,top)))),
inference(forward_demodulation,[],[f12238,f11198]) ).
fof(f12331,plain,
! [X2,X0,X1] : join(X0,join(X1,complement(composition(sk1,X2)))) = join(complement(X2),join(X0,complement(composition(sk1,complement(X1))))),
inference(forward_demodulation,[],[f12215,f2]) ).
fof(f13047,plain,
! [X0] : join(complement(one),complement(composition(sk1,X0))) = join(complement(X0),complement(sk1)),
inference(superposition,[],[f11360,f8]) ).
fof(f13157,plain,
! [X0,X1] : join(complement(composition(sk1,X0)),complement(X1)) = join(complement(X0),complement(composition(sk1,X1))),
inference(superposition,[],[f1,f11360]) ).
fof(f14205,plain,
! [X0,X1] : join(complement(composition(sk2,top)),join(X0,complement(composition(sk1,complement(X1))))) = complement(composition(sk2,composition(sk1,complement(join(X1,X0))))),
inference(superposition,[],[f8205,f11280]) ).
fof(f14228,plain,
! [X0,X1] : join(complement(composition(sk2,top)),join(X0,complement(composition(sk1,complement(X1))))) = complement(composition(sk1,composition(sk2,complement(join(X1,X0))))),
inference(forward_demodulation,[],[f14205,f11198]) ).
fof(f14368,plain,
! [X0,X1] : complement(composition(sk1,composition(sk2,complement(join(X1,X0))))) = join(X0,join(X1,complement(composition(sk1,composition(sk2,top))))),
inference(forward_demodulation,[],[f14228,f12331]) ).
fof(f14484,plain,
! [X0,X1] : complement(composition(sk1,composition(sk2,complement(join(X1,X0))))) = join(X0,complement(composition(sk1,composition(sk2,complement(X1))))),
inference(forward_demodulation,[],[f14368,f12314]) ).
fof(f15429,plain,
! [X0,X1] : complement(composition(sk2,composition(sk1,complement(join(X0,complement(X1)))))) = join(join(X0,complement(composition(sk1,X1))),complement(composition(sk2,top))),
inference(superposition,[],[f8615,f10883]) ).
fof(f15473,plain,
! [X0,X1] : join(X1,complement(composition(sk2,X0))) = join(complement(X0),join(complement(composition(sk2,top)),X1)),
inference(superposition,[],[f242,f8615]) ).
fof(f15474,plain,
! [X0,X1] : join(X1,complement(composition(sk2,X0))) = join(complement(composition(sk2,top)),join(X1,complement(X0))),
inference(superposition,[],[f242,f8615]) ).
fof(f15486,plain,
! [X0] : join(complement(composition(sk2,top)),complement(X0)) = join(complement(composition(sk2,top)),complement(composition(sk2,X0))),
inference(superposition,[],[f3496,f8615]) ).
fof(f15505,plain,
! [X0] : complement(composition(sk2,composition(sk2,X0))) = join(complement(composition(sk2,top)),complement(X0)),
inference(forward_demodulation,[],[f15486,f8205]) ).
fof(f15511,plain,
! [X0,X1] : join(X1,complement(composition(sk2,X0))) = complement(composition(sk2,complement(join(X1,complement(X0))))),
inference(forward_demodulation,[],[f15474,f10526]) ).
fof(f15512,plain,
! [X0,X1] : join(X1,complement(composition(sk2,X0))) = join(complement(X0),complement(composition(sk2,complement(X1)))),
inference(forward_demodulation,[],[f15473,f10526]) ).
fof(f15544,plain,
! [X0,X1] : complement(composition(sk2,composition(sk1,complement(join(X0,complement(X1)))))) = join(complement(composition(sk2,top)),join(X0,complement(composition(sk1,X1)))),
inference(forward_demodulation,[],[f15429,f1]) ).
fof(f15556,plain,
! [X0] : complement(composition(sk2,X0)) = complement(composition(sk2,composition(sk2,X0))),
inference(forward_demodulation,[],[f15505,f8205]) ).
fof(f15584,plain,
! [X0,X1] : complement(composition(sk2,composition(sk1,complement(join(X0,complement(X1)))))) = complement(composition(sk2,complement(join(X0,complement(composition(sk1,X1)))))),
inference(forward_demodulation,[],[f15544,f10526]) ).
fof(f15607,plain,
! [X0,X1] : complement(composition(sk2,composition(sk1,complement(join(X0,complement(X1)))))) = complement(composition(sk1,composition(sk2,complement(join(complement(X1),X0))))),
inference(forward_demodulation,[],[f15584,f11532]) ).
fof(f15618,plain,
! [X0,X1] : complement(composition(sk2,composition(sk1,complement(join(X0,complement(X1)))))) = join(X0,complement(composition(sk1,composition(sk2,complement(complement(X1)))))),
inference(forward_demodulation,[],[f15607,f14484]) ).
fof(f15625,plain,
! [X0,X1] : complement(composition(sk2,composition(sk1,complement(join(X0,complement(X1)))))) = join(X0,complement(composition(sk1,composition(sk2,X1)))),
inference(forward_demodulation,[],[f15618,f2676]) ).
fof(f15632,plain,
! [X0,X1] : join(X0,complement(composition(sk1,composition(sk2,X1)))) = complement(composition(sk1,composition(sk2,complement(join(X0,complement(X1)))))),
inference(forward_demodulation,[],[f15625,f11198]) ).
fof(f15636,plain,
! [X0,X1] : join(X0,complement(composition(sk1,composition(sk2,X1)))) = join(complement(X1),complement(composition(sk1,composition(sk2,complement(X0))))),
inference(forward_demodulation,[],[f15632,f14484]) ).
fof(f15704,plain,
! [X0,X1] : join(X1,complement(composition(sk2,X0))) = complement(composition(sk2,complement(join(complement(X0),X1)))),
inference(superposition,[],[f15511,f7838]) ).
fof(f16070,plain,
! [X0,X1] : complement(composition(sk2,complement(join(X0,X1)))) = join(X1,complement(composition(sk2,complement(X0)))),
inference(superposition,[],[f15704,f2676]) ).
fof(f16164,plain,
! [X0,X1] : join(complement(X0),complement(composition(sk2,X1))) = join(complement(X1),complement(composition(sk2,X0))),
inference(superposition,[],[f15511,f15704]) ).
fof(f17251,plain,
! [X0,X1] : join(X1,complement(composition(sk2,complement(X0)))) = join(X0,complement(composition(sk2,complement(X1)))),
inference(superposition,[],[f15512,f2676]) ).
fof(f17325,plain,
! [X0,X1] : join(X0,complement(composition(sk2,X1))) = join(complement(composition(sk2,complement(X0))),complement(X1)),
inference(superposition,[],[f1,f15512]) ).
fof(f18214,plain,
! [X0] : join(complement(one),complement(composition(sk2,X0))) = join(complement(X0),complement(sk2)),
inference(superposition,[],[f16164,f8]) ).
fof(f18308,plain,
composition(complement(join(complement(sk1),complement(sk2))),sk3) != complement(join(complement(sk3),complement(composition(sk2,composition(sk1,sk3))))),
inference(superposition,[],[f22,f16164]) ).
fof(f18403,plain,
composition(complement(join(complement(sk1),complement(sk2))),sk3) != complement(join(complement(sk3),complement(composition(sk1,composition(sk2,sk3))))),
inference(forward_demodulation,[],[f18308,f11198]) ).
fof(f18527,plain,
composition(complement(join(complement(sk1),complement(sk2))),sk3) != complement(complement(composition(sk1,composition(sk2,sk3)))),
inference(forward_demodulation,[],[f18403,f11127]) ).
fof(f18600,plain,
composition(complement(join(complement(sk1),complement(sk2))),sk3) != composition(sk1,composition(sk2,sk3)),
inference(forward_demodulation,[],[f18527,f2676]) ).
fof(f19159,plain,
complement(composition(sk2,complement(complement(sk2)))) = join(complement(sk2),complement(composition(sk2,complement(complement(one))))),
inference(superposition,[],[f16070,f3926]) ).
fof(f19354,plain,
complement(composition(sk2,complement(complement(sk2)))) = join(complement(one),complement(composition(sk2,complement(complement(sk2))))),
inference(forward_demodulation,[],[f19159,f17251]) ).
fof(f19499,plain,
complement(composition(sk2,complement(complement(sk2)))) = join(complement(complement(complement(sk2))),complement(sk2)),
inference(forward_demodulation,[],[f19354,f18214]) ).
fof(f19611,plain,
complement(composition(sk2,complement(complement(sk2)))) = join(complement(sk2),complement(complement(complement(sk2)))),
inference(forward_demodulation,[],[f19499,f1]) ).
fof(f19707,plain,
join(complement(sk2),complement(sk2)) = complement(composition(sk2,complement(complement(sk2)))),
inference(forward_demodulation,[],[f19611,f2676]) ).
fof(f19770,plain,
join(complement(sk2),complement(sk2)) = complement(composition(sk2,sk2)),
inference(forward_demodulation,[],[f19707,f2676]) ).
fof(f19801,plain,
complement(sk2) = complement(composition(sk2,sk2)),
inference(forward_demodulation,[],[f19770,f2697]) ).
fof(f20178,plain,
! [X0] : join(X0,complement(composition(sk1,composition(sk2,sk2)))) = join(complement(sk2),complement(composition(sk1,complement(X0)))),
inference(superposition,[],[f10884,f19801]) ).
fof(f20210,plain,
! [X0] : join(X0,complement(composition(sk1,composition(sk2,sk2)))) = join(X0,complement(composition(sk1,sk2))),
inference(forward_demodulation,[],[f20178,f10884]) ).
fof(f21197,plain,
complement(sk1) = complement(composition(sk1,sk1)),
inference(superposition,[],[f10917,f8]) ).
fof(f21275,plain,
! [X0,X1] : join(complement(composition(sk2,complement(X1))),complement(composition(sk1,X0))) = join(X1,complement(composition(sk2,composition(sk1,composition(sk1,X0))))),
inference(superposition,[],[f17325,f10917]) ).
fof(f21276,plain,
! [X0,X1] : join(complement(composition(sk2,complement(X1))),complement(composition(sk1,X0))) = join(X1,complement(composition(sk1,composition(sk2,composition(sk1,X0))))),
inference(forward_demodulation,[],[f21275,f11198]) ).
fof(f21339,plain,
! [X0,X1] : join(X1,complement(composition(sk2,composition(sk1,X0)))) = join(X1,complement(composition(sk1,composition(sk2,composition(sk1,X0))))),
inference(forward_demodulation,[],[f21276,f17325]) ).
fof(f21374,plain,
! [X0,X1] : join(X1,complement(composition(sk1,composition(sk2,X0)))) = join(X1,complement(composition(sk1,composition(sk2,composition(sk1,X0))))),
inference(forward_demodulation,[],[f21339,f11198]) ).
fof(f21420,plain,
! [X0] : join(complement(X0),complement(sk1)) = join(complement(sk1),complement(composition(sk1,X0))),
inference(superposition,[],[f11360,f21197]) ).
fof(f23871,plain,
! [X0] : complement(composition(sk2,complement(join(complement(X0),complement(sk1))))) = join(complement(one),complement(composition(sk2,composition(sk1,X0)))),
inference(superposition,[],[f15511,f13047]) ).
fof(f23924,plain,
! [X0] : complement(composition(sk2,complement(join(complement(X0),complement(sk1))))) = join(complement(composition(sk1,X0)),complement(sk2)),
inference(forward_demodulation,[],[f23871,f18214]) ).
fof(f23991,plain,
! [X0] : join(complement(sk2),complement(composition(sk1,X0))) = complement(composition(sk2,complement(join(complement(X0),complement(sk1))))),
inference(forward_demodulation,[],[f23924,f1]) ).
fof(f24043,plain,
! [X0] : join(complement(sk2),complement(composition(sk1,X0))) = join(complement(X0),complement(composition(sk2,sk1))),
inference(forward_demodulation,[],[f23991,f15511]) ).
fof(f24136,plain,
! [X0] : join(complement(composition(sk1,X0)),complement(composition(sk2,sk1))) = join(complement(sk2),complement(composition(sk1,composition(sk1,composition(sk1,X0))))),
inference(superposition,[],[f24043,f10917]) ).
fof(f24201,plain,
! [X0] : join(complement(sk2),complement(composition(sk1,X0))) = join(complement(sk1),complement(composition(sk2,X0))),
inference(superposition,[],[f16164,f24043]) ).
fof(f24214,plain,
! [X0] : join(X0,complement(composition(sk2,composition(sk2,sk1)))) = join(complement(sk2),complement(composition(sk1,composition(sk2,complement(X0))))),
inference(superposition,[],[f17325,f24043]) ).
fof(f24316,plain,
! [X0] : join(X0,complement(composition(sk1,composition(sk2,sk2)))) = join(X0,complement(composition(sk2,composition(sk2,sk1)))),
inference(forward_demodulation,[],[f24214,f15636]) ).
fof(f24382,plain,
! [X0] : join(complement(composition(sk1,X0)),complement(composition(sk2,sk1))) = join(complement(sk1),complement(composition(sk2,composition(sk1,composition(sk1,X0))))),
inference(forward_demodulation,[],[f24136,f24201]) ).
fof(f24433,plain,
! [X0] : join(X0,complement(composition(sk1,composition(sk2,sk2)))) = join(X0,complement(composition(sk2,sk1))),
inference(forward_demodulation,[],[f24316,f15556]) ).
fof(f24485,plain,
! [X0] : join(complement(composition(sk1,X0)),complement(composition(sk2,sk1))) = join(complement(sk1),complement(composition(sk1,composition(sk2,composition(sk1,X0))))),
inference(forward_demodulation,[],[f24382,f11198]) ).
fof(f24525,plain,
! [X0] : join(X0,complement(composition(sk1,sk2))) = join(X0,complement(composition(sk2,sk1))),
inference(forward_demodulation,[],[f24433,f20210]) ).
fof(f24567,plain,
! [X0] : join(complement(composition(sk1,X0)),complement(composition(sk2,sk1))) = join(complement(sk1),complement(composition(sk1,composition(sk2,X0)))),
inference(forward_demodulation,[],[f24485,f21374]) ).
fof(f24624,plain,
! [X0] : join(complement(composition(sk1,X0)),complement(composition(sk2,sk1))) = join(complement(composition(sk2,X0)),complement(sk1)),
inference(forward_demodulation,[],[f24567,f21420]) ).
fof(f24664,plain,
! [X0] : join(complement(sk1),complement(composition(sk2,X0))) = join(complement(composition(sk1,X0)),complement(composition(sk2,sk1))),
inference(forward_demodulation,[],[f24624,f1]) ).
fof(f24697,plain,
! [X0] : join(complement(sk1),complement(composition(sk2,X0))) = join(complement(composition(sk1,X0)),complement(composition(sk1,sk2))),
inference(forward_demodulation,[],[f24664,f24525]) ).
fof(f24722,plain,
! [X0] : join(complement(sk1),complement(composition(sk2,X0))) = join(complement(X0),complement(composition(sk1,composition(sk1,sk2)))),
inference(forward_demodulation,[],[f24697,f13157]) ).
fof(f24742,plain,
! [X0] : join(complement(sk1),complement(composition(sk2,X0))) = join(complement(X0),complement(composition(sk1,sk2))),
inference(forward_demodulation,[],[f24722,f10917]) ).
fof(f24860,plain,
complement(composition(sk1,sk2)) = join(complement(sk1),complement(composition(sk2,sk2))),
inference(superposition,[],[f3944,f24742]) ).
fof(f24986,plain,
join(complement(sk1),complement(sk2)) = complement(composition(sk1,sk2)),
inference(forward_demodulation,[],[f24860,f19801]) ).
fof(f66721,plain,
composition(sk1,composition(sk2,sk3)) != composition(complement(complement(composition(sk1,sk2))),sk3),
inference(superposition,[],[f18600,f24986]) ).
fof(f66724,plain,
composition(sk1,composition(sk2,sk3)) != composition(composition(sk1,sk2),sk3),
inference(forward_demodulation,[],[f66721,f2676]) ).
fof(f66726,plain,
$false,
inference(forward_subsumption_resolution,[],[f66724,f7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL029-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n001.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 22:59:17 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.27/2.78 % (4060053)Detected a unit-equality problem, will run specialized UEQ schedule.
% 13.27/2.78 % (4060059)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=445198786:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 13.27/2.78 % (4060060)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=3766309460:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 13.27/2.78 % (4060061)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1439496704:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 13.27/2.78 % (4060062)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=171732347:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 13.27/2.78 % (4060058)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=1597290495:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 13.27/2.78 % (4060063)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1897547344:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 13.27/2.78 % (4060064)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3013716844:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 13.27/2.78 % (4060061)Instruction limit reached!
% 13.27/2.78 % (4060061)------------------------------
% 13.27/2.78 % (4060061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.78 % (4060061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.78 % (4060061)CaDiCaL version: 2.1.3
% 13.27/2.78 % (4060061)Termination reason: Instruction limit
% 13.27/2.78 % (4060061)Termination phase: Saturation
% 13.27/2.78 % (4060061)Time elapsed: 0.083 s
% 13.27/2.78 % (4060061)Peak memory usage: 89 MB
% 13.27/2.78 % (4060061)Instructions burned: 136 (million)
% 13.27/2.78 % (4060062)Instruction limit reached!
% 13.27/2.78 % (4060062)------------------------------
% 13.27/2.78 % (4060062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.78 % (4060062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.78 % (4060062)CaDiCaL version: 2.1.3
% 13.27/2.78 % (4060062)Termination reason: Instruction limit
% 13.27/2.78 % (4060062)Termination phase: Saturation
% 13.27/2.78 % (4060062)Time elapsed: 0.105 s
% 13.27/2.78 % (4060062)Peak memory usage: 89 MB
% 13.27/2.78 % (4060062)Instructions burned: 182 (million)
% 13.27/2.78 % (4060063)Instruction limit reached!
% 13.27/2.78 % (4060063)------------------------------
% 13.27/2.78 % (4060063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.78 % (4060063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.78 % (4060063)CaDiCaL version: 2.1.3
% 13.27/2.78 % (4060063)Termination reason: Instruction limit
% 13.27/2.78 % (4060063)Termination phase: Saturation
% 13.27/2.78 % (4060063)Time elapsed: 0.167 s
% 13.27/2.78 % (4060063)Peak memory usage: 90 MB
% 13.27/2.78 % (4060063)Instructions burned: 257 (million)
% 13.27/2.78 % (4060072)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2804309679:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 13.27/2.78 % (4060073)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=248514861:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 13.27/2.78 % (4060074)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3891168244:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 13.27/2.78 % (4060074)Instruction limit reached!
% 13.27/2.78 % (4060074)------------------------------
% 13.27/2.78 % (4060074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.78 % (4060074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.78 % (4060074)CaDiCaL version: 2.1.3
% 13.27/2.78 % (4060074)Termination reason: Instruction limit
% 13.27/2.78 % (4060074)Termination phase: Saturation
% 13.27/2.78 % (4060074)Time elapsed: 0.119 s
% 13.27/2.78 % (4060074)Peak memory usage: 92 MB
% 13.27/2.78 % (4060074)Instructions burned: 215 (million)
% 13.27/2.78 % (4060078)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=2136248040:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi)
% 13.27/2.78 % (4060064)Instruction limit reached!
% 13.27/2.78 % (4060064)------------------------------
% 13.27/2.78 % (4060064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.78 % (4060064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.78 % (4060064)CaDiCaL version: 2.1.3
% 13.27/2.78 % (4060064)Termination reason: Instruction limit
% 13.27/2.78 % (4060064)Termination phase: Saturation
% 13.27/2.78 % (4060064)Time elapsed: 0.638 s
% 13.27/2.78 % (4060064)Peak memory usage: 100 MB
% 13.27/2.78 % (4060064)Instructions burned: 1187 (million)
% 13.27/2.78 % (4060078)Instruction limit reached!
% 13.27/2.78 % (4060078)------------------------------
% 13.27/2.78 % (4060078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.78 % (4060078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.78 % (4060078)CaDiCaL version: 2.1.3
% 13.27/2.78 % (4060078)Termination reason: Instruction limit
% 13.27/2.78 % (4060078)Termination phase: Saturation
% 13.27/2.78 % (4060078)Time elapsed: 0.198 s
% 13.27/2.78 % (4060078)Peak memory usage: 93 MB
% 13.27/2.78 % (4060078)Instructions burned: 318 (million)
% 13.27/2.78 % (4060080)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=786011149:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/12125Mi)
% 13.27/2.78 % (4060081)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3966447840:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2990 on theBenchmark for (2990ds/2836Mi)
% 13.27/2.78 % (4060072)Instruction limit reached!
% 13.27/2.78 % (4060072)------------------------------
% 13.27/2.78 % (4060072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.27/2.78 % (4060072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.27/2.78 % (4060072)CaDiCaL version: 2.1.3
% 13.27/2.78 % (4060072)Termination reason: Instruction limit
% 13.27/2.78 % (4060072)Termination phase: Saturation
% 13.27/2.78 % (4060072)Time elapsed: 1.281 s
% 13.27/2.78 % (4060072)Peak memory usage: 140 MB
% 13.27/2.78 % (4060072)Instructions burned: 2051 (million)
% 13.27/2.78 % (4060059)First to succeed.
% 13.27/2.78 % (4060059)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4060053"
% 13.27/2.78 % (4060084)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3211207686:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2983 on theBenchmark for (2983ds/14534Mi)
% 13.27/2.78 % (4060059)Refutation found. Thanks to Tanya!
% 13.27/2.78 % SZS status Unsatisfiable for theBenchmark
% 13.27/2.78 % SZS output start Proof for theBenchmark
% See solution above
% 14.16/2.98 % (4060059)------------------------------
% 14.16/2.98 % (4060059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.16/2.98 % (4060059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.16/2.98 % (4060059)CaDiCaL version: 2.1.3
% 14.16/2.98 % (4060059)Termination reason: Refutation
% 14.16/2.98 % (4060059)Time elapsed: 1.622 s
% 14.16/2.98 % (4060059)Peak memory usage: 160 MB
% 14.16/2.98 % (4060059)Instructions burned: 4864 (million)
% 14.16/2.98 % (4060059)------------------------------
% 14.16/2.98 % (4060059)------------------------------
% 14.16/2.98 % (4060053)Success in time 1.917 s
% 14.16/2.98 % Vampire exiting
%------------------------------------------------------------------------------