%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT017-1 : TPTP v9.3.1. Bugfixed v2.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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:03:08 PM UTC 2026
% Result : Unsatisfiable 32.71s 4.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT017-1 : TPTP v9.3.1. Bugfixed v2.2.1.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n005.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 23:06:32 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 32.71/4.65 % Refutation found
% 32.71/4.65 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 32.71/4.65 % SZS output start CNFRefutation for theBenchmark
% 32.71/4.65 fof(f1,axiom,(
% 32.71/4.65 (![X]: (join(complement(X),X) = n1 ))),
% 32.71/4.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.71/4.65 fof(f2,axiom,(
% 32.71/4.65 (![X]: (meet(complement(X),X) = n0 ))),
% 32.71/4.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.71/4.65 fof(f3,axiom,(
% 32.71/4.65 (![X,Y]: (join(X,meet(X,Y)) = X ))),
% 32.71/4.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.71/4.65 fof(f4,axiom,(
% 32.71/4.65 (![X,Y]: (meet(X,Y) = meet(Y,X) ))),
% 32.71/4.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.71/4.65 fof(f5,axiom,(
% 32.71/4.65 (![X,Y]: (join(X,Y) = join(Y,X) ))),
% 32.71/4.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.71/4.65 fof(f6,axiom,(
% 32.71/4.65 (![X,Y,Z]: (meet(meet(X,Y),Z) = meet(X,meet(Y,Z)) ))),
% 32.71/4.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.71/4.65 fof(f7,axiom,(
% 32.71/4.65 (![X,Y,Z]: (join(join(X,Y),Z) = join(X,join(Y,Z)) ))),
% 32.71/4.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.71/4.65 fof(f8,axiom,(
% 32.71/4.65 (![X]: (complement(complement(X)) = X ))),
% 32.71/4.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.71/4.65 fof(f10,axiom,(
% 32.71/4.65 (![X,Y]: (meet(X,Y) = complement(join(complement(X),complement(Y))) ))),
% 32.71/4.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.71/4.65 fof(f11,negated_conjecture,(
% 32.71/4.65 join(a,join(meet(complement(a),meet(join(a,complement(b)),join(a,b))),meet(complement(a),join(meet(complement(a),b),meet(complement(a),complement(b)))))) != n1 ),
% 32.71/4.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 32.71/4.65 fof(f12,plain,(
% 32.71/4.65 ![X0]: (join(complement(X0),X0)=n1)),
% 32.71/4.65 inference(cnf_transformation,[status(thm)],[f1])).
% 32.71/4.65 fof(f13,plain,(
% 32.71/4.65 ![X0]: (meet(complement(X0),X0)=n0)),
% 32.71/4.65 inference(cnf_transformation,[status(thm)],[f2])).
% 32.71/4.65 fof(f14,plain,(
% 32.71/4.65 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 32.71/4.65 inference(cnf_transformation,[status(thm)],[f3])).
% 32.71/4.65 fof(f15,plain,(
% 32.71/4.65 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 32.71/4.65 inference(cnf_transformation,[status(thm)],[f4])).
% 32.71/4.65 fof(f16,plain,(
% 32.71/4.65 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 32.71/4.65 inference(cnf_transformation,[status(thm)],[f5])).
% 32.71/4.65 fof(f17,plain,(
% 32.71/4.65 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X0,meet(X1,X2)))),
% 32.71/4.65 inference(cnf_transformation,[status(thm)],[f6])).
% 32.71/4.65 fof(f18,plain,(
% 32.71/4.65 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X1,X2)))),
% 32.71/4.65 inference(cnf_transformation,[status(thm)],[f7])).
% 32.71/4.65 fof(f19,plain,(
% 32.71/4.65 ![X0]: (complement(complement(X0))=X0)),
% 32.71/4.65 inference(cnf_transformation,[status(thm)],[f8])).
% 32.71/4.65 fof(f21,plain,(
% 32.71/4.65 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 32.71/4.65 inference(cnf_transformation,[status(thm)],[f10])).
% 32.71/4.65 fof(f22,plain,(
% 32.71/4.65 ~join(a,join(meet(complement(a),meet(join(a,complement(b)),join(a,b))),meet(complement(a),join(meet(complement(a),b),meet(complement(a),complement(b))))))=n1),
% 32.71/4.65 inference(cnf_transformation,[status(thm)],[f11])).
% 32.71/4.65 fof(f23,definition,(
% 32.71/4.65 sF3_fnc=complement(a)),
% 32.71/4.65 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 32.71/4.65 fof(f24,definition,(
% 32.71/4.65 sF6_fnc=complement(b)),
% 32.71/4.65 introduced(definition,[new_symbols(definition,[sF6_fnc])],[function_definition])).
% 32.71/4.65 fof(f25,definition,(
% 32.71/4.65 sF5_fnc=join(a,sF6_fnc)),
% 32.71/4.65 introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition])).
% 32.71/4.65 fof(f26,definition,(
% 32.71/4.65 sF7_fnc=join(a,b)),
% 32.71/4.65 introduced(definition,[new_symbols(definition,[sF7_fnc])],[function_definition])).
% 32.71/4.65 fof(f27,definition,(
% 32.71/4.65 sF4_fnc=meet(sF5_fnc,sF7_fnc)),
% 32.71/4.65 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 32.71/4.65 fof(f28,definition,(
% 32.71/4.65 sF2_fnc=meet(sF3_fnc,sF4_fnc)),
% 32.71/4.65 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 32.71/4.65 fof(f29,definition,(
% 32.71/4.65 sF10_fnc=meet(sF3_fnc,b)),
% 32.71/4.65 introduced(definition,[new_symbols(definition,[sF10_fnc])],[function_definition])).
% 32.71/4.65 fof(f30,definition,(
% 32.71/4.65 sF11_fnc=meet(sF3_fnc,sF6_fnc)),
% 32.71/4.65 introduced(definition,[new_symbols(definition,[sF11_fnc])],[function_definition])).
% 32.71/4.65 fof(f31,definition,(
% 32.71/4.65 sF9_fnc=join(sF10_fnc,sF11_fnc)),
% 32.71/4.65 introduced(definition,[new_symbols(definition,[sF9_fnc])],[function_definition])).
% 32.71/4.65 fof(f32,definition,(
% 32.71/4.65 sF8_fnc=meet(sF3_fnc,sF9_fnc)),
% 32.71/4.65 introduced(definition,[new_symbols(definition,[sF8_fnc])],[function_definition])).
% 32.71/4.65 fof(f33,definition,(
% 32.71/4.65 sF1_fnc=join(sF2_fnc,sF8_fnc)),
% 32.71/4.65 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 32.71/4.65 fof(f34,definition,(
% 32.71/4.65 sF0_fnc=join(a,sF1_fnc)),
% 32.71/4.65 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 32.71/4.65 fof(f35,plain,(
% 32.71/4.65 ~sF0_fnc=n1),
% 32.71/4.65 inference(definition_folding,[],[f22,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23])).
% 32.71/4.65 fof(f37,plain,(
% 32.71/4.65 complement(sF6_fnc)=b),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f24,f19])).
% 32.71/4.65 fof(f38,plain,(
% 32.71/4.65 complement(sF3_fnc)=a),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f23,f19])).
% 32.71/4.65 fof(f43,plain,(
% 32.71/4.65 ![X0]: (join(X0,complement(X0))=n1)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f19,f12])).
% 32.71/4.65 fof(f53,plain,(
% 32.71/4.65 sF10_fnc=meet(b,sF3_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f29,f15])).
% 32.71/4.65 fof(f60,plain,(
% 32.71/4.65 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f15,f14])).
% 32.71/4.65 fof(f69,plain,(
% 32.71/4.65 ![X0]: (meet(X0,complement(X0))=n0)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f15,f13])).
% 32.71/4.65 fof(f96,plain,(
% 32.71/4.65 ![X0]: (join(X0,n0)=X0)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f69,f14])).
% 32.71/4.65 fof(f102,plain,(
% 32.71/4.65 n1=complement(n0)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f12,f96])).
% 32.71/4.65 fof(f111,plain,(
% 32.71/4.65 join(sF9_fnc,sF8_fnc)=sF9_fnc),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f32,f60])).
% 32.71/4.65 fof(f125,plain,(
% 32.71/4.65 ![X0]: (X0=join(n0,X0))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f96,f16])).
% 32.71/4.65 fof(f149,plain,(
% 32.71/4.65 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X1,meet(X2,X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f15,f17])).
% 32.71/4.65 fof(f156,plain,(
% 32.71/4.65 ![X0]: (meet(sF10_fnc,X0)=meet(b,meet(sF3_fnc,X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f53,f17])).
% 32.71/4.65 fof(f158,plain,(
% 32.71/4.65 ![X0]: (meet(sF8_fnc,X0)=meet(sF3_fnc,meet(sF9_fnc,X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f32,f17])).
% 32.71/4.65 fof(f159,plain,(
% 32.71/4.65 ![X0]: (meet(sF11_fnc,X0)=meet(sF3_fnc,meet(sF6_fnc,X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f30,f17])).
% 32.71/4.65 fof(f161,plain,(
% 32.71/4.65 ![X0]: (meet(sF2_fnc,X0)=meet(sF3_fnc,meet(sF4_fnc,X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f28,f17])).
% 32.71/4.65 fof(f162,plain,(
% 32.71/4.65 ![X0]: (meet(sF4_fnc,X0)=meet(sF5_fnc,meet(sF7_fnc,X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f27,f17])).
% 32.71/4.65 fof(f164,plain,(
% 32.71/4.65 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X1,meet(X0,X2)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f15,f17])).
% 32.71/4.65 fof(f167,plain,(
% 32.71/4.65 ![X0,X1,X2]: (join(X0,meet(X1,meet(X2,X0)))=X0)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f17,f60])).
% 32.71/4.65 fof(f175,plain,(
% 32.71/4.65 ![X0,X1,X2]: (join(X0,X1)=join(X0,join(X1,meet(X2,join(X0,X1)))))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f60,f18])).
% 32.71/4.65 fof(f177,plain,(
% 32.71/4.65 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X2,X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f16,f18])).
% 32.71/4.65 fof(f190,plain,(
% 32.71/4.65 ![X0]: (join(sF1_fnc,X0)=join(sF2_fnc,join(sF8_fnc,X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f33,f18])).
% 32.71/4.65 fof(f191,plain,(
% 32.71/4.65 ![X0]: (join(sF9_fnc,X0)=join(sF10_fnc,join(sF11_fnc,X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f31,f18])).
% 32.71/4.65 fof(f193,plain,(
% 32.71/4.65 ![X0]: (join(sF0_fnc,X0)=join(a,join(sF1_fnc,X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f34,f18])).
% 32.71/4.65 fof(f194,plain,(
% 32.71/4.65 ![X0]: (join(sF7_fnc,X0)=join(a,join(b,X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f26,f18])).
% 32.71/4.65 fof(f195,plain,(
% 32.71/4.65 ![X0]: (join(sF5_fnc,X0)=join(a,join(sF6_fnc,X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f25,f18])).
% 32.71/4.65 fof(f198,plain,(
% 32.71/4.65 ![X0,X1,X2]: (join(X0,X1)=join(X0,join(meet(X2,X0),X1)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f60,f18])).
% 32.71/4.65 fof(f295,plain,(
% 32.71/4.65 ![X0,X1]: (meet(complement(X0),X1)=complement(join(X0,complement(X1))))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f19,f21])).
% 32.71/4.65 fof(f301,plain,(
% 32.71/4.65 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),X1)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f19,f21])).
% 32.71/4.65 fof(f308,plain,(
% 32.71/4.65 ![X0,X1]: (complement(meet(X0,X1))=join(complement(X0),complement(X1)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f21,f19])).
% 32.71/4.65 fof(f343,plain,(
% 32.71/4.65 ![X0,X1,X2]: (join(X0,meet(meet(X1,X0),X2))=X0)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f15,f167])).
% 32.71/4.65 fof(f368,plain,(
% 32.71/4.65 ![X0,X1,X2]: (join(X0,meet(X1,meet(X0,X2)))=X0)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f17,f343])).
% 32.71/4.65 fof(f694,plain,(
% 32.71/4.65 ![X0]: (meet(complement(n0),X0)=complement(complement(X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f125,f295])).
% 32.71/4.65 fof(f698,plain,(
% 32.71/4.65 ![X0,X1]: (meet(complement(X0),X1)=complement(join(complement(X1),X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f16,f295])).
% 32.71/4.65 fof(f702,plain,(
% 32.71/4.65 ![X0]: (meet(complement(X0),sF3_fnc)=complement(join(X0,a)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f38,f295])).
% 32.71/4.65 fof(f711,plain,(
% 32.71/4.65 ![X0,X1]: (complement(meet(complement(X0),X1))=join(X0,complement(X1)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f295,f19])).
% 32.71/4.65 fof(f712,plain,(
% 32.71/4.65 ![X0]: (meet(n1,X0)=complement(complement(X0)))),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f102,f694])).
% 32.71/4.65 fof(f713,plain,(
% 32.71/4.65 ![X0]: (meet(n1,X0)=X0)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f19,f712])).
% 32.71/4.65 fof(f735,plain,(
% 32.71/4.65 ![X0,X1]: (join(X0,X1)=join(X0,join(X0,X1)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f713,f198])).
% 32.71/4.65 fof(f740,plain,(
% 32.71/4.65 ![X0]: (join(X0,X0)=X0)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f713,f60])).
% 32.71/4.65 fof(f759,plain,(
% 32.71/4.65 ![X0]: (meet(complement(complement(X0)),X0)=complement(complement(X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f740,f295])).
% 32.71/4.65 fof(f761,plain,(
% 32.71/4.65 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f19,f759])).
% 32.71/4.65 fof(f762,plain,(
% 32.71/4.65 ![X0]: (meet(X0,X0)=X0)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f19,f761])).
% 32.71/4.65 fof(f797,plain,(
% 32.71/4.65 ![X0,X1]: (meet(X0,meet(meet(X1,X0),X1))=meet(X1,X0))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f149,f762])).
% 32.71/4.65 fof(f802,plain,(
% 32.71/4.65 meet(sF8_fnc,sF9_fnc)=meet(sF3_fnc,sF9_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f762,f158])).
% 32.71/4.65 fof(f811,plain,(
% 32.71/4.65 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X1,X0))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f762,f149])).
% 32.71/4.65 fof(f820,plain,(
% 32.71/4.65 ![X0,X1]: (meet(X0,meet(X0,meet(X1,X1)))=meet(X1,X0))),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f164,f797])).
% 32.71/4.65 fof(f822,plain,(
% 32.71/4.65 ![X0,X1]: (meet(X0,meet(X0,X1))=meet(X1,X0))),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f762,f820])).
% 32.71/4.65 fof(f823,plain,(
% 32.71/4.65 meet(sF8_fnc,sF9_fnc)=sF8_fnc),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f32,f802])).
% 32.71/4.65 fof(f862,plain,(
% 32.71/4.65 join(sF10_fnc,sF11_fnc)=join(sF10_fnc,sF9_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f31,f735])).
% 32.71/4.65 fof(f865,plain,(
% 32.71/4.65 join(a,b)=join(a,sF7_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f26,f735])).
% 32.71/4.65 fof(f877,plain,(
% 32.71/4.65 ![X0,X1]: (join(X0,X1)=join(X0,join(X1,X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f16,f735])).
% 32.71/4.65 fof(f902,plain,(
% 32.71/4.65 sF9_fnc=join(sF10_fnc,sF9_fnc)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f31,f862])).
% 32.71/4.65 fof(f905,plain,(
% 32.71/4.65 sF7_fnc=join(a,sF7_fnc)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f26,f865])).
% 32.71/4.65 fof(f949,plain,(
% 32.71/4.65 meet(sF8_fnc,sF8_fnc)=meet(sF9_fnc,sF8_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f823,f822])).
% 32.71/4.65 fof(f962,plain,(
% 32.71/4.65 meet(sF3_fnc,sF11_fnc)=meet(sF6_fnc,sF3_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f30,f822])).
% 32.71/4.65 fof(f964,plain,(
% 32.71/4.65 meet(sF3_fnc,sF2_fnc)=meet(sF4_fnc,sF3_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f28,f822])).
% 32.71/4.65 fof(f965,plain,(
% 32.71/4.65 meet(sF5_fnc,sF4_fnc)=meet(sF7_fnc,sF5_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f27,f822])).
% 32.71/4.65 fof(f999,plain,(
% 32.71/4.65 sF8_fnc=meet(sF9_fnc,sF8_fnc)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f762,f949])).
% 32.71/4.65 fof(f1084,plain,(
% 32.71/4.65 meet(sF11_fnc,sF6_fnc)=meet(sF3_fnc,sF6_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f762,f159])).
% 32.71/4.65 fof(f1106,plain,(
% 32.71/4.65 meet(sF11_fnc,sF6_fnc)=sF11_fnc),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f30,f1084])).
% 32.71/4.65 fof(f1175,plain,(
% 32.71/4.65 meet(sF2_fnc,sF4_fnc)=meet(sF3_fnc,sF4_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f762,f161])).
% 32.71/4.65 fof(f1195,plain,(
% 32.71/4.65 meet(sF2_fnc,sF4_fnc)=sF2_fnc),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f28,f1175])).
% 32.71/4.65 fof(f1243,plain,(
% 32.71/4.65 meet(sF6_fnc,sF11_fnc)=sF11_fnc),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f15,f1106])).
% 32.71/4.65 fof(f1279,plain,(
% 32.71/4.65 meet(sF2_fnc,sF2_fnc)=meet(sF4_fnc,sF2_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f1195,f822])).
% 32.71/4.65 fof(f1289,plain,(
% 32.71/4.65 sF2_fnc=meet(sF4_fnc,sF2_fnc)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f762,f1279])).
% 32.71/4.65 fof(f1292,plain,(
% 32.71/4.65 meet(sF8_fnc,sF8_fnc)=meet(sF3_fnc,sF8_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f999,f158])).
% 32.71/4.65 fof(f1306,plain,(
% 32.71/4.65 sF8_fnc=meet(sF3_fnc,sF8_fnc)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f762,f1292])).
% 32.71/4.65 fof(f1315,plain,(
% 32.71/4.65 meet(sF4_fnc,sF7_fnc)=meet(sF5_fnc,sF7_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f762,f162])).
% 32.71/4.65 fof(f1335,plain,(
% 32.71/4.65 meet(sF4_fnc,sF7_fnc)=sF4_fnc),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f27,f1315])).
% 32.71/4.65 fof(f1377,plain,(
% 32.71/4.65 meet(sF11_fnc,sF11_fnc)=meet(sF3_fnc,sF11_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f1243,f159])).
% 32.71/4.65 fof(f1388,plain,(
% 32.71/4.65 sF11_fnc=meet(sF6_fnc,sF3_fnc)),
% 32.71/4.65 inference(backward_demodulation,[status(thm)],[f1389,f962])).
% 32.71/4.65 fof(f1389,plain,(
% 32.71/4.65 sF11_fnc=meet(sF3_fnc,sF11_fnc)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f762,f1377])).
% 32.71/4.65 fof(f1491,plain,(
% 32.71/4.65 meet(sF2_fnc,sF2_fnc)=meet(sF3_fnc,sF2_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f1289,f161])).
% 32.71/4.65 fof(f1504,plain,(
% 32.71/4.65 sF2_fnc=meet(sF4_fnc,sF3_fnc)),
% 32.71/4.65 inference(backward_demodulation,[status(thm)],[f1505,f964])).
% 32.71/4.65 fof(f1505,plain,(
% 32.71/4.65 sF2_fnc=meet(sF3_fnc,sF2_fnc)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f762,f1491])).
% 32.71/4.65 fof(f1991,plain,(
% 32.71/4.65 meet(sF4_fnc,sF4_fnc)=meet(sF7_fnc,sF4_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f1335,f822])).
% 32.71/4.65 fof(f2003,plain,(
% 32.71/4.65 sF4_fnc=meet(sF7_fnc,sF4_fnc)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f762,f1991])).
% 32.71/4.65 fof(f2077,plain,(
% 32.71/4.65 meet(sF4_fnc,sF4_fnc)=meet(sF5_fnc,sF4_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f2003,f162])).
% 32.71/4.65 fof(f2092,plain,(
% 32.71/4.65 sF4_fnc=meet(sF7_fnc,sF5_fnc)),
% 32.71/4.65 inference(backward_demodulation,[status(thm)],[f2093,f965])).
% 32.71/4.65 fof(f2093,plain,(
% 32.71/4.65 sF4_fnc=meet(sF5_fnc,sF4_fnc)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f762,f2077])).
% 32.71/4.65 fof(f2253,plain,(
% 32.71/4.65 join(sF11_fnc,sF10_fnc)=join(sF11_fnc,sF9_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f31,f877])).
% 32.71/4.65 fof(f2258,plain,(
% 32.71/4.65 join(sF1_fnc,a)=join(sF1_fnc,sF0_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f34,f877])).
% 32.71/4.65 fof(f2259,plain,(
% 32.71/4.65 join(b,a)=join(b,sF7_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f26,f877])).
% 32.71/4.65 fof(f2260,plain,(
% 32.71/4.65 join(sF6_fnc,a)=join(sF6_fnc,sF5_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f25,f877])).
% 32.71/4.65 fof(f2402,plain,(
% 32.71/4.65 ![X0,X1,X2,X3]: (join(X0,X1)=join(X1,join(meet(X2,meet(X1,X3)),X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f368,f177])).
% 32.71/4.65 fof(f2454,plain,(
% 32.71/4.65 ![X0]: (join(sF7_fnc,join(X0,a))=join(X0,sF7_fnc))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f905,f177])).
% 32.71/4.65 fof(f2737,plain,(
% 32.71/4.65 join(sF1_fnc,a)=join(sF0_fnc,sF1_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f16,f2258])).
% 32.71/4.65 fof(f2761,plain,(
% 32.71/4.65 join(sF7_fnc,b)=join(sF7_fnc,join(b,a))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f2259,f877])).
% 32.71/4.65 fof(f2765,plain,(
% 32.71/4.65 join(sF7_fnc,b)=join(b,sF7_fnc)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f2454,f2761])).
% 32.71/4.65 fof(f2766,plain,(
% 32.71/4.65 join(sF7_fnc,b)=join(b,a)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f2259,f2765])).
% 32.71/4.65 fof(f2789,plain,(
% 32.71/4.65 join(sF0_fnc,sF1_fnc)=join(a,sF1_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f740,f193])).
% 32.71/4.65 fof(f2818,plain,(
% 32.71/4.65 join(sF1_fnc,a)=sF0_fnc),
% 32.71/4.65 inference(backward_demodulation,[status(thm)],[f2819,f2737])).
% 32.71/4.65 fof(f2819,plain,(
% 32.71/4.65 join(sF0_fnc,sF1_fnc)=sF0_fnc),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f34,f2789])).
% 32.71/4.65 fof(f2959,plain,(
% 32.71/4.65 join(sF10_fnc,sF11_fnc)=join(sF11_fnc,sF9_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f16,f2253])).
% 32.71/4.65 fof(f2970,plain,(
% 32.71/4.65 join(sF11_fnc,sF10_fnc)=sF9_fnc),
% 32.71/4.65 inference(backward_demodulation,[status(thm)],[f2971,f2253])).
% 32.71/4.65 fof(f2971,plain,(
% 32.71/4.65 sF9_fnc=join(sF11_fnc,sF9_fnc)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f31,f2959])).
% 32.71/4.65 fof(f3022,plain,(
% 32.71/4.65 join(sF6_fnc,a)=join(sF5_fnc,sF6_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f16,f2260])).
% 32.71/4.65 fof(f3063,plain,(
% 32.71/4.65 join(sF7_fnc,b)=join(a,b)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f740,f194])).
% 32.71/4.65 fof(f3096,plain,(
% 32.71/4.65 sF7_fnc=join(b,a)),
% 32.71/4.65 inference(backward_demodulation,[status(thm)],[f3097,f2766])).
% 32.71/4.65 fof(f3097,plain,(
% 32.71/4.65 join(sF7_fnc,b)=sF7_fnc),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f26,f3063])).
% 32.71/4.65 fof(f3137,plain,(
% 32.71/4.65 join(sF5_fnc,sF6_fnc)=join(a,sF6_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f740,f195])).
% 32.71/4.65 fof(f3167,plain,(
% 32.71/4.65 join(sF6_fnc,a)=sF5_fnc),
% 32.71/4.65 inference(backward_demodulation,[status(thm)],[f3168,f3022])).
% 32.71/4.65 fof(f3168,plain,(
% 32.71/4.65 join(sF5_fnc,sF6_fnc)=sF5_fnc),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f25,f3137])).
% 32.71/4.65 fof(f4510,plain,(
% 32.71/4.65 meet(sF10_fnc,sF8_fnc)=meet(b,sF8_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f1306,f156])).
% 32.71/4.65 fof(f4517,plain,(
% 32.71/4.65 meet(sF10_fnc,sF9_fnc)=meet(b,sF8_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f32,f156])).
% 32.71/4.65 fof(f4906,plain,(
% 32.71/4.65 meet(sF9_fnc,sF10_fnc)=meet(b,sF8_fnc)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f15,f4517])).
% 32.71/4.65 fof(f4981,plain,(
% 32.71/4.65 ![X0,X1]: (meet(X0,complement(meet(complement(X0),X1)))=complement(complement(X0)))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f14,f301])).
% 32.71/4.65 fof(f5019,plain,(
% 32.71/4.65 ![X0,X1]: (meet(X0,join(X0,complement(X1)))=complement(complement(X0)))),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f711,f4981])).
% 32.71/4.65 fof(f5020,plain,(
% 32.71/4.65 ![X0,X1]: (meet(X0,join(X0,complement(X1)))=X0)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f19,f5019])).
% 32.71/4.65 fof(f5045,plain,(
% 32.71/4.65 ![X0]: (complement(meet(X0,sF3_fnc))=join(complement(X0),a))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f38,f308])).
% 32.71/4.65 fof(f5117,plain,(
% 32.71/4.65 ![X0,X1]: (meet(join(X0,complement(X1)),X0)=meet(X0,join(X0,complement(X1))))),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f5020,f811])).
% 32.71/4.65 fof(f5149,plain,(
% 32.71/4.65 ![X0,X1]: (meet(join(X0,complement(X1)),X0)=X0)),
% 32.71/4.65 inference(forward_demodulation,[status(thm)],[f5020,f5117])).
% 32.71/4.65 fof(f5179,plain,(
% 32.71/4.65 ![X0,X1]: (meet(join(X0,X1),X0)=X0)),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f19,f5149])).
% 32.71/4.65 fof(f5408,plain,(
% 32.71/4.65 meet(sF9_fnc,sF11_fnc)=sF11_fnc),
% 32.71/4.65 inference(paramodulation,[status(thm)],[f2970,f5179])).
% 32.71/4.66 fof(f5472,plain,(
% 32.71/4.66 meet(sF9_fnc,sF10_fnc)=sF10_fnc),
% 32.71/4.66 inference(paramodulation,[status(thm)],[f902,f5179])).
% 32.71/4.66 fof(f5535,plain,(
% 32.71/4.66 sF10_fnc=meet(b,sF8_fnc)),
% 32.71/4.66 inference(backward_demodulation,[status(thm)],[f5472,f4906])).
% 32.71/4.66 fof(f5553,plain,(
% 32.71/4.66 meet(sF10_fnc,sF8_fnc)=sF10_fnc),
% 32.71/4.66 inference(backward_demodulation,[status(thm)],[f5535,f4510])).
% 32.71/4.66 fof(f5629,plain,(
% 32.71/4.66 meet(sF8_fnc,sF11_fnc)=meet(sF3_fnc,sF11_fnc)),
% 32.71/4.66 inference(paramodulation,[status(thm)],[f5408,f158])).
% 32.71/4.66 fof(f5646,plain,(
% 32.71/4.66 meet(sF8_fnc,sF11_fnc)=sF11_fnc),
% 32.71/4.66 inference(forward_demodulation,[status(thm)],[f1389,f5629])).
% 32.71/4.66 fof(f6422,plain,(
% 32.71/4.66 meet(sF8_fnc,sF11_fnc)=meet(sF11_fnc,sF8_fnc)),
% 32.71/4.66 inference(paramodulation,[status(thm)],[f5646,f822])).
% 32.71/4.66 fof(f6435,plain,(
% 32.71/4.66 sF11_fnc=meet(sF11_fnc,sF8_fnc)),
% 32.71/4.66 inference(forward_demodulation,[status(thm)],[f5646,f6422])).
% 32.71/4.66 fof(f7279,plain,(
% 32.71/4.66 ![X0,X1,X2,X3]: (join(X0,meet(X1,meet(X0,X2)))=join(X0,join(meet(X1,meet(X0,X2)),meet(X3,X0))))),
% 32.71/4.66 inference(paramodulation,[status(thm)],[f368,f175])).
% 32.71/4.66 fof(f7539,plain,(
% 32.71/4.66 ![X0,X1,X2,X3]: (X0=join(X0,join(meet(X1,meet(X0,X2)),meet(X3,X0))))),
% 32.71/4.66 inference(forward_demodulation,[status(thm)],[f368,f7279])).
% 32.71/4.66 fof(f7552,plain,(
% 32.71/4.66 ![X0,X1]: (X0=join(meet(X1,X0),X0))),
% 32.71/4.66 inference(forward_demodulation,[status(thm)],[f2402,f7539])).
% 32.71/4.66 fof(f8897,plain,(
% 32.71/4.66 sF8_fnc=join(sF11_fnc,sF8_fnc)),
% 32.71/4.66 inference(paramodulation,[status(thm)],[f6435,f7552])).
% 32.71/4.66 fof(f8905,plain,(
% 32.71/4.66 sF8_fnc=join(sF10_fnc,sF8_fnc)),
% 32.71/4.66 inference(paramodulation,[status(thm)],[f5553,f7552])).
% 32.71/4.66 fof(f9273,plain,(
% 32.71/4.66 join(sF9_fnc,sF8_fnc)=join(sF10_fnc,sF8_fnc)),
% 32.71/4.66 inference(paramodulation,[status(thm)],[f8897,f191])).
% 32.71/4.66 fof(f9287,plain,(
% 32.71/4.66 sF9_fnc=join(sF10_fnc,sF8_fnc)),
% 32.71/4.66 inference(forward_demodulation,[status(thm)],[f111,f9273])).
% 32.71/4.66 fof(f9313,plain,(
% 32.71/4.66 sF8_fnc=join(sF10_fnc,sF11_fnc)),
% 32.71/4.66 inference(backward_demodulation,[status(thm)],[f9438,f31])).
% 32.71/4.66 fof(f9438,plain,(
% 32.71/4.66 sF9_fnc=sF8_fnc),
% 32.71/4.66 inference(forward_demodulation,[status(thm)],[f8905,f9287])).
% 32.71/4.66 fof(f21630,plain,(
% 32.71/4.66 meet(b,sF3_fnc)=complement(join(sF6_fnc,a))),
% 32.71/4.66 inference(paramodulation,[status(thm)],[f37,f702])).
% 32.71/4.70 fof(f21632,plain,(
% 32.71/4.70 meet(sF6_fnc,sF3_fnc)=complement(join(b,a))),
% 32.71/4.70 inference(paramodulation,[status(thm)],[f24,f702])).
% 32.71/4.70 fof(f21685,plain,(
% 32.71/4.70 sF10_fnc=complement(join(sF6_fnc,a))),
% 32.71/4.70 inference(forward_demodulation,[status(thm)],[f53,f21630])).
% 32.71/4.70 fof(f21707,plain,(
% 32.71/4.70 sF10_fnc=complement(sF5_fnc)),
% 32.71/4.70 inference(forward_demodulation,[status(thm)],[f3167,f21685])).
% 32.71/4.70 fof(f21710,plain,(
% 32.71/4.70 sF11_fnc=complement(join(b,a))),
% 32.71/4.70 inference(forward_demodulation,[status(thm)],[f1388,f21632])).
% 32.71/4.70 fof(f21732,plain,(
% 32.71/4.70 sF11_fnc=complement(sF7_fnc)),
% 32.71/4.70 inference(forward_demodulation,[status(thm)],[f3096,f21710])).
% 32.71/4.70 fof(f22140,plain,(
% 32.71/4.70 ![X0]: (meet(complement(X0),sF5_fnc)=complement(join(sF10_fnc,X0)))),
% 32.71/4.70 inference(paramodulation,[status(thm)],[f21707,f698])).
% 32.71/4.70 fof(f22195,plain,(
% 32.71/4.70 complement(sF11_fnc)=sF7_fnc),
% 32.71/4.70 inference(paramodulation,[status(thm)],[f21732,f19])).
% 32.71/4.70 fof(f44343,plain,(
% 32.71/4.70 meet(sF7_fnc,sF5_fnc)=complement(join(sF10_fnc,sF11_fnc))),
% 32.71/4.70 inference(paramodulation,[status(thm)],[f22195,f22140])).
% 32.71/4.70 fof(f44418,plain,(
% 32.71/4.70 sF4_fnc=complement(join(sF10_fnc,sF11_fnc))),
% 32.71/4.70 inference(forward_demodulation,[status(thm)],[f2092,f44343])).
% 32.71/4.70 fof(f44435,plain,(
% 32.71/4.70 sF4_fnc=complement(sF8_fnc)),
% 32.71/4.70 inference(forward_demodulation,[status(thm)],[f9313,f44418])).
% 32.71/4.70 fof(f44544,plain,(
% 32.71/4.70 complement(sF4_fnc)=sF8_fnc),
% 32.71/4.70 inference(paramodulation,[status(thm)],[f44435,f19])).
% 32.71/4.70 fof(f44630,plain,(
% 32.71/4.70 complement(meet(sF4_fnc,sF3_fnc))=join(sF8_fnc,a)),
% 32.71/4.70 inference(paramodulation,[status(thm)],[f44544,f5045])).
% 32.71/4.70 fof(f44660,plain,(
% 32.71/4.70 complement(sF2_fnc)=join(sF8_fnc,a)),
% 32.71/4.70 inference(forward_demodulation,[status(thm)],[f1504,f44630])).
% 32.71/4.70 fof(f45417,plain,(
% 32.71/4.70 join(sF1_fnc,a)=join(sF2_fnc,complement(sF2_fnc))),
% 32.71/4.70 inference(paramodulation,[status(thm)],[f44660,f190])).
% 32.71/4.70 fof(f45448,plain,(
% 32.71/4.70 sF0_fnc=join(sF2_fnc,complement(sF2_fnc))),
% 32.71/4.70 inference(forward_demodulation,[status(thm)],[f2818,f45417])).
% 32.71/4.70 fof(f45449,plain,(
% 32.71/4.70 sF0_fnc=n1),
% 32.71/4.70 inference(forward_demodulation,[status(thm)],[f43,f45448])).
% 32.71/4.70 fof(f45450,plain,(
% 32.71/4.70 $false),
% 32.71/4.70 inference(forward_subsumption_resolution,[status(thm)],[f45449,f35])).
% 32.71/4.70 % SZS output end CNFRefutation for theBenchmark.p
% 8.93/4.72 % Elapsed time: 4.345408 seconds
% 8.93/4.72 % CPU time: 34.263091 seconds
% 8.93/4.72 % Total memory used: 211.360 MB
% 8.93/4.72 % Net memory used: 205.193 MB
%------------------------------------------------------------------------------