%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL109-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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 : Thu Sep 24 01:09:22 PM UTC 2026
% Result : Unsatisfiable 98.54s 12.99s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL109-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n013.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Mon Sep 21 00:04:36 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 98.54/12.99 % Refutation found
% 98.54/12.99 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 98.54/12.99 % SZS output start CNFRefutation for theBenchmark
% 98.54/12.99 fof(f1,axiom,(
% 98.54/12.99 (![X]: (implies(truth,X) = X ))),
% 98.54/12.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 98.54/12.99 fof(f2,axiom,(
% 98.54/12.99 (![X,Y,Z]: (implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))) = truth ))),
% 98.54/12.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 98.54/12.99 fof(f3,axiom,(
% 98.54/12.99 (![X,Y]: (implies(implies(X,Y),Y) = implies(implies(Y,X),X) ))),
% 98.54/12.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 98.54/12.99 fof(f4,axiom,(
% 98.54/12.99 (![X,Y]: (implies(implies(not(X),not(Y)),implies(Y,X)) = truth ))),
% 98.54/12.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 98.54/12.99 fof(f5,negated_conjecture,(
% 98.54/12.99 implies(implies(implies(a,b),implies(b,a)),implies(b,a)) != truth ),
% 98.54/12.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 98.54/12.99 fof(f6,plain,(
% 98.54/12.99 ![X0]: (implies(truth,X0)=X0)),
% 98.54/12.99 inference(cnf_transformation,[status(thm)],[f1])).
% 98.54/12.99 fof(f7,plain,(
% 98.54/12.99 ![X0,X1,X2]: (implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))=truth)),
% 98.54/12.99 inference(cnf_transformation,[status(thm)],[f2])).
% 98.54/12.99 fof(f8,plain,(
% 98.54/12.99 ![X0,X1]: (implies(implies(X0,X1),X1)=implies(implies(X1,X0),X0))),
% 98.54/12.99 inference(cnf_transformation,[status(thm)],[f3])).
% 98.54/12.99 fof(f9,plain,(
% 98.54/12.99 ![X0,X1]: (implies(implies(not(X0),not(X1)),implies(X1,X0))=truth)),
% 98.54/12.99 inference(cnf_transformation,[status(thm)],[f4])).
% 98.54/12.99 fof(f10,plain,(
% 98.54/12.99 ~implies(implies(implies(a,b),implies(b,a)),implies(b,a))=truth),
% 98.54/12.99 inference(cnf_transformation,[status(thm)],[f5])).
% 98.54/12.99 fof(f11,definition,(
% 98.54/12.99 sF2_fnc=implies(a,b)),
% 98.54/12.99 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 98.54/12.99 fof(f12,definition,(
% 98.54/12.99 sF3_fnc=implies(b,a)),
% 98.54/12.99 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 98.54/12.99 fof(f13,definition,(
% 98.54/12.99 sF1_fnc=implies(sF2_fnc,sF3_fnc)),
% 98.54/12.99 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 98.54/12.99 fof(f14,definition,(
% 98.54/12.99 sF0_fnc=implies(sF1_fnc,sF3_fnc)),
% 98.54/12.99 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 98.54/12.99 fof(f15,plain,(
% 98.54/12.99 ~sF0_fnc=truth),
% 98.54/12.99 inference(definition_folding,[],[f10,f14,f13,f12,f11])).
% 98.54/12.99 fof(f16,plain,(
% 98.54/12.99 ![X0,X1,X2,X3]: (implies(truth,implies(implies(implies(implies(X0,X1),implies(X2,X1)),X3),implies(implies(X2,X0),X3)))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f7,f7])).
% 98.54/12.99 fof(f17,plain,(
% 98.54/12.99 ![X0]: (implies(sF1_fnc,implies(implies(sF3_fnc,X0),implies(sF2_fnc,X0)))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f13,f7])).
% 98.54/12.99 fof(f20,plain,(
% 98.54/12.99 ![X0,X1]: (implies(X0,implies(implies(X0,X1),implies(truth,X1)))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f6,f7])).
% 98.54/12.99 fof(f22,plain,(
% 98.54/12.99 ![X0,X1,X2,X3]: (implies(implies(X0,implies(X1,X2)),implies(truth,implies(X0,implies(implies(X2,X3),implies(X1,X3)))))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f7,f7])).
% 98.54/12.99 fof(f26,plain,(
% 98.54/12.99 ![X0,X1]: (implies(implies(X0,truth),implies(X1,implies(X0,X1)))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f6,f7])).
% 98.54/12.99 fof(f32,plain,(
% 98.54/12.99 ![X0,X1,X2,X3]: (implies(implies(implies(implies(X0,X1),implies(X2,X1)),X3),implies(implies(X2,X0),X3))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f16])).
% 98.54/12.99 fof(f33,plain,(
% 98.54/12.99 ![X0,X1]: (implies(X0,implies(implies(X0,X1),X1))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f20])).
% 98.54/12.99 fof(f34,plain,(
% 98.54/12.99 ![X0,X1,X2,X3]: (implies(implies(X0,implies(X1,X2)),implies(X0,implies(implies(X2,X3),implies(X1,X3))))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f22])).
% 98.54/12.99 fof(f41,plain,(
% 98.54/12.99 ![X0,X1,X2]: (implies(truth,implies(implies(X0,X1),implies(X2,X1)))=implies(implies(implies(implies(X0,X1),implies(X2,X1)),implies(X2,X0)),implies(X2,X0)))),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f7,f8])).
% 98.54/12.99 fof(f42,plain,(
% 98.54/12.99 implies(sF3_fnc,a)=implies(implies(a,b),b)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f12,f8])).
% 98.54/12.99 fof(f43,plain,(
% 98.54/12.99 ![X0]: (implies(X0,X0)=implies(implies(X0,truth),truth))),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f6,f8])).
% 98.54/12.99 fof(f55,plain,(
% 98.54/12.99 ![X0,X1,X2]: (implies(implies(X0,X1),implies(X2,X1))=implies(implies(implies(implies(X0,X1),implies(X2,X1)),implies(X2,X0)),implies(X2,X0)))),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f41])).
% 98.54/12.99 fof(f56,plain,(
% 98.54/12.99 implies(sF3_fnc,a)=implies(sF2_fnc,b)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f11,f42])).
% 98.54/12.99 fof(f59,plain,(
% 98.54/12.99 implies(implies(a,sF3_fnc),sF3_fnc)=implies(implies(sF2_fnc,b),a)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f56,f8])).
% 98.54/12.99 fof(f84,plain,(
% 98.54/12.99 ![X0]: (implies(implies(truth,X0),X0)=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f6,f33])).
% 98.54/12.99 fof(f85,plain,(
% 98.54/12.99 ![X0]: (implies(X0,implies(X0,X0))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f43,f33])).
% 98.54/12.99 fof(f96,plain,(
% 98.54/12.99 implies(a,implies(sF2_fnc,b))=truth),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f11,f33])).
% 98.54/12.99 fof(f114,plain,(
% 98.54/12.99 ![X0]: (implies(X0,X0)=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f84])).
% 98.54/12.99 fof(f119,plain,(
% 98.54/12.99 ![X0,X1]: (implies(truth,implies(X0,implies(X1,X0)))=truth)),
% 98.54/12.99 inference(backward_demodulation,[status(thm)],[f120,f26])).
% 98.54/12.99 fof(f120,plain,(
% 98.54/12.99 ![X0]: (implies(X0,truth)=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f114,f85])).
% 98.54/12.99 fof(f148,plain,(
% 98.54/12.99 ![X0,X1]: (implies(X0,implies(X1,X0))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f119])).
% 98.54/12.99 fof(f158,plain,(
% 98.54/12.99 ![X0]: (implies(implies(not(X0),not(truth)),X0)=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f6,f9])).
% 98.54/12.99 fof(f235,plain,(
% 98.54/12.99 implies(a,sF3_fnc)=truth),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f12,f148])).
% 98.54/12.99 fof(f247,plain,(
% 98.54/12.99 ![X0,X1]: (implies(implies(implies(X0,X1),X1),X1)=implies(truth,implies(X0,X1)))),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f148,f8])).
% 98.54/12.99 fof(f252,plain,(
% 98.54/12.99 implies(truth,sF3_fnc)=implies(implies(sF2_fnc,b),a)),
% 98.54/12.99 inference(backward_demodulation,[status(thm)],[f235,f59])).
% 98.54/12.99 fof(f254,plain,(
% 98.54/12.99 ![X0,X1]: (implies(implies(implies(X0,X1),X1),X1)=implies(X0,X1))),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f247])).
% 98.54/12.99 fof(f259,plain,(
% 98.54/12.99 sF3_fnc=implies(implies(sF2_fnc,b),a)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f252])).
% 98.54/12.99 fof(f490,plain,(
% 98.54/12.99 ![X0,X1]: (implies(implies(implies(X0,X1),X1),X0)=implies(X1,X0))),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f8,f254])).
% 98.54/12.99 fof(f509,plain,(
% 98.54/12.99 implies(implies(sF2_fnc,b),b)=implies(a,b)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f11,f254])).
% 98.54/12.99 fof(f550,plain,(
% 98.54/12.99 implies(implies(sF2_fnc,b),b)=sF2_fnc),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f11,f509])).
% 98.54/12.99 fof(f2128,plain,(
% 98.54/12.99 ![X0,X1,X2,X3]: (implies(truth,implies(implies(X0,X1),implies(implies(X1,X2),implies(implies(X2,X3),implies(X0,X3)))))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f34,f32])).
% 98.54/12.99 fof(f2344,plain,(
% 98.54/12.99 ![X0,X1,X2,X3]: (implies(implies(X0,X1),implies(implies(X1,X2),implies(implies(X2,X3),implies(X0,X3))))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f2128])).
% 98.54/12.99 fof(f2413,plain,(
% 98.54/12.99 ![X0,X1,X2,X3]: (implies(truth,implies(implies(implies(X0,X1),X2),implies(implies(X2,X3),implies(X1,X3))))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f148,f2344])).
% 98.54/12.99 fof(f2617,plain,(
% 98.54/12.99 ![X0,X1,X2,X3]: (implies(implies(implies(X0,X1),X2),implies(implies(X2,X3),implies(X1,X3)))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f2413])).
% 98.54/12.99 fof(f2887,plain,(
% 98.54/12.99 ![X0,X1,X2,X3,X4]: (implies(implies(implies(X0,X1),implies(X2,X3)),implies(truth,implies(X1,implies(implies(X3,X4),implies(X2,X4)))))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f7,f2617])).
% 98.54/12.99 fof(f3053,plain,(
% 98.54/12.99 ![X0,X1,X2,X3,X4]: (implies(implies(implies(X0,X1),implies(X2,X3)),implies(X1,implies(implies(X3,X4),implies(X2,X4))))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f2887])).
% 98.54/12.99 fof(f4972,plain,(
% 98.54/12.99 ![X0,X1,X2]: (implies(truth,implies(not(X0),implies(implies(X1,X2),implies(X0,X2))))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f9,f3053])).
% 98.54/12.99 fof(f5267,plain,(
% 98.54/12.99 ![X0,X1,X2]: (implies(not(X0),implies(implies(X1,X2),implies(X0,X2)))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f4972])).
% 98.54/12.99 fof(f5633,plain,(
% 98.54/12.99 ![X0,X1]: (implies(not(X0),implies(truth,implies(X0,X1)))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f158,f5267])).
% 98.54/12.99 fof(f5774,plain,(
% 98.54/12.99 ![X0,X1]: (implies(not(X0),implies(X0,X1))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f5633])).
% 98.54/12.99 fof(f5968,plain,(
% 98.54/12.99 ![X0,X1,X2,X3]: (implies(implies(implies(X0,X1),not(X2)),implies(truth,implies(X1,implies(X2,X3))))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f5774,f2617])).
% 98.54/12.99 fof(f5990,plain,(
% 98.54/12.99 ![X0,X1]: (implies(implies(implies(X0,X1),not(X0)),not(X0))=implies(truth,implies(X0,X1)))),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f5774,f8])).
% 98.54/12.99 fof(f6025,plain,(
% 98.54/12.99 ![X0,X1,X2,X3]: (implies(implies(implies(X0,X1),not(X2)),implies(X1,implies(X2,X3)))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f5968])).
% 98.54/12.99 fof(f6063,plain,(
% 98.54/12.99 ![X0,X1]: (implies(implies(implies(X0,X1),not(X0)),not(X0))=implies(X0,X1))),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f5990])).
% 98.54/12.99 fof(f6813,plain,(
% 98.54/12.99 ![X0,X1,X2,X3]: (implies(implies(implies(X0,X1),not(X2)),implies(not(X0),implies(X2,X3)))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f6063,f6025])).
% 98.54/12.99 fof(f6946,plain,(
% 98.54/12.99 ![X0,X1,X2,X3,X4]: (implies(truth,implies(implies(implies(X0,X1),not(X2)),implies(implies(implies(X2,X3),X4),implies(X1,X4))))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f6025,f34])).
% 98.54/12.99 fof(f7100,plain,(
% 98.54/12.99 ![X0,X1,X2,X3,X4]: (implies(implies(implies(X0,X1),not(X2)),implies(implies(implies(X2,X3),X4),implies(X1,X4)))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f6946])).
% 98.54/12.99 fof(f7176,plain,(
% 98.54/12.99 ![X0,X1]: (implies(truth,implies(not(not(not(X0))),implies(X0,X1)))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f158,f6813])).
% 98.54/12.99 fof(f7347,plain,(
% 98.54/12.99 ![X0,X1]: (implies(not(not(not(X0))),implies(X0,X1))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f7176])).
% 98.54/12.99 fof(f7588,plain,(
% 98.54/12.99 ![X0,X1,X2,X3]: (implies(implies(implies(X0,X1),not(not(not(X2)))),implies(truth,implies(X1,implies(X2,X3))))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f7347,f2617])).
% 98.54/12.99 fof(f7647,plain,(
% 98.54/12.99 ![X0,X1,X2,X3]: (implies(implies(implies(X0,X1),not(not(not(X2)))),implies(X1,implies(X2,X3)))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f7588])).
% 98.54/12.99 fof(f10833,plain,(
% 98.54/12.99 ![X0,X1,X2,X3]: (implies(truth,implies(not(not(not(X0))),implies(implies(implies(X0,X1),X2),implies(X3,X2))))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f7647,f3053])).
% 98.54/12.99 fof(f11039,plain,(
% 98.54/12.99 ![X0,X1,X2,X3]: (implies(not(not(not(X0))),implies(implies(implies(X0,X1),X2),implies(X3,X2)))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f10833])).
% 98.54/12.99 fof(f11519,plain,(
% 98.54/12.99 ![X0,X1]: (implies(not(not(not(not(X0)))),implies(truth,implies(X1,X0)))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f158,f11039])).
% 98.54/12.99 fof(f11747,plain,(
% 98.54/12.99 ![X0,X1]: (implies(not(not(not(not(X0)))),implies(X1,X0))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f11519])).
% 98.54/12.99 fof(f12062,plain,(
% 98.54/12.99 ![X0]: (implies(not(not(not(not(X0)))),X0)=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f6,f11747])).
% 98.54/12.99 fof(f12244,plain,(
% 98.54/12.99 ![X0]: (implies(truth,implies(X0,not(not(not(not(X0))))))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f12062,f9])).
% 98.54/12.99 fof(f12334,plain,(
% 98.54/12.99 ![X0]: (implies(X0,not(not(not(not(X0)))))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f12244])).
% 98.54/12.99 fof(f12763,plain,(
% 98.54/12.99 ![X0]: (implies(implies(not(not(not(not(X0)))),X0),X0)=implies(truth,not(not(not(not(X0))))))),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f12334,f8])).
% 98.54/12.99 fof(f12881,plain,(
% 98.54/12.99 ![X0]: (implies(truth,X0)=implies(truth,not(not(not(not(X0))))))),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f12062,f12763])).
% 98.54/12.99 fof(f12882,plain,(
% 98.54/12.99 ![X0]: (X0=implies(truth,not(not(not(not(X0))))))),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f12881])).
% 98.54/12.99 fof(f12940,plain,(
% 98.54/12.99 ![X0]: (X0=not(not(not(not(X0)))))),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f12882])).
% 98.54/12.99 fof(f12989,plain,(
% 98.54/12.99 ![X0,X1]: (implies(implies(X0,not(X1)),implies(X1,not(not(not(X0)))))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f12940,f9])).
% 98.54/12.99 fof(f13125,plain,(
% 98.54/12.99 ![X0,X1]: (implies(implies(implies(X0,not(not(not(X1)))),implies(X1,not(X0))),implies(X1,not(X0)))=implies(truth,implies(X0,not(not(not(X1))))))),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f12989,f8])).
% 98.54/12.99 fof(f13237,plain,(
% 98.54/12.99 ![X0,X1]: (implies(implies(implies(X0,not(not(not(X1)))),implies(X1,not(X0))),implies(X1,not(X0)))=implies(X0,not(not(not(X1)))))),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f13125])).
% 98.54/12.99 fof(f28432,plain,(
% 98.54/12.99 ![X0,X1,X2]: (implies(implies(implies(X0,X1),not(not(X2))),implies(truth,implies(X1,X2)))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f158,f7100])).
% 98.54/12.99 fof(f28864,plain,(
% 98.54/12.99 ![X0,X1,X2]: (implies(implies(implies(X0,X1),not(not(X2))),implies(X1,X2))=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f28432])).
% 98.54/12.99 fof(f30840,plain,(
% 98.54/12.99 ![X0,X1]: (implies(implies(X0,not(not(X1))),implies(X0,X1))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f490,f28864])).
% 98.54/12.99 fof(f31026,plain,(
% 98.54/12.99 ![X0,X1]: (implies(implies(implies(X0,truth),not(not(X1))),X1)=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f6,f28864])).
% 98.54/12.99 fof(f31237,plain,(
% 98.54/12.99 ![X0]: (implies(implies(truth,not(not(X0))),X0)=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f120,f31026])).
% 98.54/12.99 fof(f31242,plain,(
% 98.54/12.99 ![X0]: (implies(not(not(X0)),X0)=truth)),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f6,f31237])).
% 98.54/12.99 fof(f31428,plain,(
% 98.54/12.99 ![X0]: (implies(X0,not(not(X0)))=truth)),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f12940,f31242])).
% 98.54/12.99 fof(f31833,plain,(
% 98.54/12.99 ![X0,X1]: (implies(implies(X0,not(not(X0))),implies(X1,not(not(X0))))=implies(implies(implies(truth,implies(X1,not(not(X0)))),implies(X1,X0)),implies(X1,X0)))),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f31428,f55])).
% 98.54/12.99 fof(f31934,plain,(
% 98.54/12.99 ![X0]: (implies(implies(not(not(X0)),X0),X0)=implies(truth,not(not(X0))))),
% 98.54/12.99 inference(paramodulation,[status(thm)],[f31428,f8])).
% 98.54/12.99 fof(f31976,plain,(
% 98.54/12.99 ![X0,X1]: (implies(truth,implies(X0,not(not(X1))))=implies(implies(implies(truth,implies(X0,not(not(X1)))),implies(X0,X1)),implies(X0,X1)))),
% 98.54/12.99 inference(forward_demodulation,[status(thm)],[f31428,f31833])).
% 98.54/12.99 fof(f31977,plain,(
% 98.54/12.99 ![X0,X1]: (implies(X0,not(not(X1)))=implies(implies(implies(truth,implies(X0,not(not(X1)))),implies(X0,X1)),implies(X0,X1)))),
% 98.54/13.00 inference(forward_demodulation,[status(thm)],[f6,f31976])).
% 98.54/13.00 fof(f31978,plain,(
% 98.54/13.00 ![X0,X1]: (implies(X0,not(not(X1)))=implies(implies(implies(X0,not(not(X1))),implies(X0,X1)),implies(X0,X1)))),
% 98.54/13.00 inference(forward_demodulation,[status(thm)],[f6,f31977])).
% 98.54/13.00 fof(f31979,plain,(
% 98.54/13.00 ![X0,X1]: (implies(X0,not(not(X1)))=implies(truth,implies(X0,X1)))),
% 98.54/13.00 inference(forward_demodulation,[status(thm)],[f30840,f31978])).
% 98.54/13.00 fof(f31982,plain,(
% 98.54/13.00 ![X0,X1]: (implies(implies(X0,not(X1)),implies(X1,not(X0)))=truth)),
% 98.54/13.00 inference(backward_demodulation,[status(thm)],[f32237,f12989])).
% 98.54/13.00 fof(f32198,plain,(
% 98.54/13.00 ![X0,X1]: (implies(implies(implies(X0,not(not(not(X1)))),implies(X1,not(X0))),implies(X1,not(X0)))=implies(X0,not(X1)))),
% 98.54/13.00 inference(backward_demodulation,[status(thm)],[f32237,f13237])).
% 98.54/13.00 fof(f32237,plain,(
% 98.54/13.00 ![X0,X1]: (implies(X0,not(not(X1)))=implies(X0,X1))),
% 98.54/13.00 inference(forward_demodulation,[status(thm)],[f6,f31979])).
% 98.54/13.00 fof(f32421,plain,(
% 98.54/13.00 ![X0]: (implies(truth,X0)=implies(truth,not(not(X0))))),
% 98.54/13.00 inference(forward_demodulation,[status(thm)],[f31242,f31934])).
% 98.54/13.00 fof(f32422,plain,(
% 98.54/13.00 ![X0]: (X0=implies(truth,not(not(X0))))),
% 98.54/13.00 inference(forward_demodulation,[status(thm)],[f6,f32421])).
% 98.54/13.00 fof(f32859,plain,(
% 98.54/13.00 ![X0]: (X0=not(not(X0)))),
% 98.54/13.00 inference(forward_demodulation,[status(thm)],[f6,f32422])).
% 98.54/13.00 fof(f32936,plain,(
% 98.54/13.00 ![X0,X1]: (implies(implies(implies(X0,not(X1)),implies(X1,not(X0))),implies(X1,not(X0)))=implies(X0,not(X1)))),
% 98.54/13.00 inference(forward_demodulation,[status(thm)],[f32237,f32198])).
% 98.54/13.00 fof(f32937,plain,(
% 98.54/13.00 ![X0,X1]: (implies(truth,implies(X0,not(X1)))=implies(X1,not(X0)))),
% 98.54/13.00 inference(forward_demodulation,[status(thm)],[f31982,f32936])).
% 98.54/13.00 fof(f32938,plain,(
% 98.54/13.00 ![X0,X1]: (implies(X0,not(X1))=implies(X1,not(X0)))),
% 98.54/13.00 inference(forward_demodulation,[status(thm)],[f6,f32937])).
% 98.54/13.00 fof(f33060,plain,(
% 98.54/13.00 ![X0,X1]: (implies(implies(not(X0),X1),X1)=implies(X0,not(implies(X1,not(X0)))))),
% 98.54/13.00 inference(paramodulation,[status(thm)],[f8,f32938])).
% 98.54/13.00 fof(f33062,plain,(
% 98.54/13.00 ![X0]: (not(X0)=implies(X0,not(truth)))),
% 98.54/13.00 inference(paramodulation,[status(thm)],[f6,f32938])).
% 100.07/13.20 fof(f33066,plain,(
% 100.07/13.20 ![X0,X1]: (implies(X0,X1)=implies(not(X1),not(X0)))),
% 100.07/13.20 inference(paramodulation,[status(thm)],[f32859,f32938])).
% 100.07/13.20 fof(f36041,plain,(
% 100.07/13.20 ![X0,X1]: (implies(implies(X0,not(not(X1))),not(X0))=implies(X1,not(implies(not(X0),not(X1)))))),
% 100.07/13.20 inference(paramodulation,[status(thm)],[f32938,f33060])).
% 100.07/13.20 fof(f36367,plain,(
% 100.07/13.20 ![X0,X1]: (implies(implies(X0,X1),not(X0))=implies(X1,not(implies(not(X0),not(X1)))))),
% 100.07/13.20 inference(forward_demodulation,[status(thm)],[f32859,f36041])).
% 100.07/13.20 fof(f36368,plain,(
% 100.07/13.20 ![X0,X1]: (implies(implies(X0,X1),not(X0))=implies(X1,not(implies(X1,X0))))),
% 100.07/13.20 inference(forward_demodulation,[status(thm)],[f33066,f36367])).
% 100.07/13.20 fof(f36635,plain,(
% 100.07/13.20 implies(sF2_fnc,not(implies(sF2_fnc,b)))=implies(b,not(implies(b,implies(sF2_fnc,b))))),
% 100.07/13.20 inference(paramodulation,[status(thm)],[f550,f36368])).
% 100.07/13.20 fof(f36636,plain,(
% 100.07/13.20 implies(sF3_fnc,not(implies(sF2_fnc,b)))=implies(a,not(implies(a,implies(sF2_fnc,b))))),
% 100.07/13.20 inference(paramodulation,[status(thm)],[f259,f36368])).
% 100.07/13.20 fof(f37046,plain,(
% 100.07/13.20 implies(sF2_fnc,not(implies(sF2_fnc,b)))=implies(b,not(truth))),
% 100.07/13.20 inference(forward_demodulation,[status(thm)],[f148,f36635])).
% 100.07/13.20 fof(f37058,plain,(
% 100.07/13.20 implies(sF2_fnc,not(implies(sF2_fnc,b)))=not(b)),
% 100.07/13.20 inference(forward_demodulation,[status(thm)],[f33062,f37046])).
% 100.07/13.20 fof(f37059,plain,(
% 100.07/13.20 implies(sF3_fnc,not(implies(sF2_fnc,b)))=implies(a,not(truth))),
% 100.07/13.20 inference(forward_demodulation,[status(thm)],[f96,f36636])).
% 100.07/13.20 fof(f37072,plain,(
% 100.07/13.20 implies(sF3_fnc,not(implies(sF2_fnc,b)))=not(a)),
% 100.07/13.20 inference(forward_demodulation,[status(thm)],[f33062,f37059])).
% 100.07/13.20 fof(f38791,plain,(
% 100.07/13.20 implies(sF1_fnc,implies(implies(sF3_fnc,not(implies(sF2_fnc,b))),not(b)))=truth),
% 100.07/13.20 inference(paramodulation,[status(thm)],[f37058,f17])).
% 100.07/13.20 fof(f38886,plain,(
% 100.07/13.20 implies(sF1_fnc,implies(not(a),not(b)))=truth),
% 100.07/13.20 inference(forward_demodulation,[status(thm)],[f37072,f38791])).
% 100.07/13.20 fof(f38887,plain,(
% 100.07/13.20 implies(sF1_fnc,implies(b,a))=truth),
% 100.07/13.20 inference(forward_demodulation,[status(thm)],[f33066,f38886])).
% 100.07/13.20 fof(f38888,plain,(
% 100.07/13.20 sF0_fnc=truth),
% 100.07/13.20 inference(backward_demodulation,[status(thm)],[f38889,f14])).
% 100.07/13.20 fof(f38889,plain,(
% 100.07/13.20 implies(sF1_fnc,sF3_fnc)=truth),
% 100.07/13.20 inference(forward_demodulation,[status(thm)],[f12,f38887])).
% 100.07/13.20 fof(f38984,plain,(
% 100.07/13.20 $false),
% 100.07/13.20 inference(forward_subsumption_resolution,[status(thm)],[f38888,f15])).
% 100.07/13.20 % SZS output end CNFRefutation for theBenchmark.p
% 27.94/13.26 % Elapsed time: 12.809514 seconds
% 27.94/13.26 % CPU time: 100.787033 seconds
% 27.94/13.26 % Total memory used: 775.525 MB
% 27.94/13.26 % Net memory used: 755.959 MB
%------------------------------------------------------------------------------