%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR049+1 : TPTP v9.3.1. Released v3.4.0.
% 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 12:14:48 PM UTC 2026
% Result : Theorem 0.12s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR049+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n005.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Mon Sep 21 14:34:33 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 0.12/0.42 % Refutation found
% 0.12/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.42 fof(f7,axiom,(
% 0.12/0.42 genls(c_tptpcol_2_2,c_tptpcol_1_1) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f9,axiom,(
% 0.12/0.42 genls(c_tptpcol_3_16386,c_tptpcol_2_2) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f11,axiom,(
% 0.12/0.42 genls(c_tptpcol_4_24578,c_tptpcol_3_16386) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f13,axiom,(
% 0.12/0.42 genls(c_tptpcol_5_24579,c_tptpcol_4_24578) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f15,axiom,(
% 0.12/0.42 genls(c_tptpcol_6_26627,c_tptpcol_5_24579) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f17,axiom,(
% 0.12/0.42 genls(c_tptpcol_7_26628,c_tptpcol_6_26627) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f19,axiom,(
% 0.12/0.42 genls(c_tptpcol_8_26629,c_tptpcol_7_26628) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f21,axiom,(
% 0.12/0.42 genls(c_tptpcol_9_26885,c_tptpcol_8_26629) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f23,axiom,(
% 0.12/0.42 genls(c_tptpcol_10_26886,c_tptpcol_9_26885) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f25,axiom,(
% 0.12/0.42 genls(c_tptpcol_11_26887,c_tptpcol_10_26886) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f27,axiom,(
% 0.12/0.42 genls(c_tptpcol_12_26919,c_tptpcol_11_26887) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f29,axiom,(
% 0.12/0.42 genls(c_tptpcol_13_26920,c_tptpcol_12_26919) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f31,axiom,(
% 0.12/0.42 genls(c_tptpcol_14_26921,c_tptpcol_13_26920) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f33,axiom,(
% 0.12/0.42 genls(c_tptpcol_15_26925,c_tptpcol_14_26921) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f35,axiom,(
% 0.12/0.42 genls(c_tptpcol_16_26926,c_tptpcol_15_26925) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f37,axiom,(
% 0.12/0.42 genls(c_tptpcol_2_65537,c_tptpcol_1_65536) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f39,axiom,(
% 0.12/0.42 genls(c_tptpcol_3_81921,c_tptpcol_2_65537) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f41,axiom,(
% 0.12/0.42 genls(c_tptpcol_4_90113,c_tptpcol_3_81921) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f43,axiom,(
% 0.12/0.42 genls(c_tptpcol_5_90114,c_tptpcol_4_90113) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f45,axiom,(
% 0.12/0.42 genls(c_tptpcol_6_92162,c_tptpcol_5_90114) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f47,axiom,(
% 0.12/0.42 genls(c_tptpcol_7_92163,c_tptpcol_6_92162) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f49,axiom,(
% 0.12/0.42 genls(c_tptpcol_8_92164,c_tptpcol_7_92163) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f51,axiom,(
% 0.12/0.42 genls(c_tptpcol_9_92165,c_tptpcol_8_92164) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f53,axiom,(
% 0.12/0.42 genls(c_tptpcol_10_92166,c_tptpcol_9_92165) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f55,axiom,(
% 0.12/0.42 genls(c_tptpcol_11_92230,c_tptpcol_10_92166) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f57,axiom,(
% 0.12/0.42 genls(c_tptpcol_12_92262,c_tptpcol_11_92230) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f59,axiom,(
% 0.12/0.42 genls(c_tptpcol_13_92263,c_tptpcol_12_92262) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f61,axiom,(
% 0.12/0.42 genls(c_tptpcol_14_92264,c_tptpcol_13_92263) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f63,axiom,(
% 0.12/0.42 genls(c_tptpcol_15_92268,c_tptpcol_14_92264) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f65,axiom,(
% 0.12/0.42 genls(c_tptpcol_16_92269,c_tptpcol_15_92268) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f67,axiom,(
% 0.12/0.42 disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f85,axiom,(
% 0.12/0.42 (! [ARG1,OLD,NEW] :( ( disjointwith(ARG1,OLD)& genls(NEW,OLD) )=> disjointwith(ARG1,NEW) ) )),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f86,axiom,(
% 0.12/0.42 (! [OLD,ARG2,NEW] :( ( disjointwith(OLD,ARG2)& genls(NEW,OLD) )=> disjointwith(NEW,ARG2) ) )),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f155,axiom,(
% 0.12/0.42 (! [X,Y,Z] :( ( genls(X,Y)& genls(Y,Z) )=> genls(X,Z) ) )),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f177,conjecture,(
% 0.12/0.42 ( mtvisible(c_unitedstatesgeographypeoplemt)=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f178,negated_conjecture,(
% 0.12/0.42 ~(( mtvisible(c_unitedstatesgeographypeoplemt)=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ) )),
% 0.12/0.42 inference(negated_conjecture,[status(cth)],[f177])).
% 0.12/0.42 fof(f185,plain,(
% 0.12/0.42 genls(c_tptpcol_2_2,c_tptpcol_1_1)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.42 fof(f188,plain,(
% 0.12/0.42 genls(c_tptpcol_3_16386,c_tptpcol_2_2)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.42 fof(f191,plain,(
% 0.12/0.42 genls(c_tptpcol_4_24578,c_tptpcol_3_16386)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f11])).
% 0.12/0.42 fof(f194,plain,(
% 0.12/0.42 genls(c_tptpcol_5_24579,c_tptpcol_4_24578)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f13])).
% 0.12/0.42 fof(f197,plain,(
% 0.12/0.42 genls(c_tptpcol_6_26627,c_tptpcol_5_24579)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f15])).
% 0.12/0.42 fof(f200,plain,(
% 0.12/0.42 genls(c_tptpcol_7_26628,c_tptpcol_6_26627)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f17])).
% 0.12/0.42 fof(f203,plain,(
% 0.12/0.42 genls(c_tptpcol_8_26629,c_tptpcol_7_26628)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f19])).
% 0.12/0.42 fof(f206,plain,(
% 0.12/0.42 genls(c_tptpcol_9_26885,c_tptpcol_8_26629)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f21])).
% 0.12/0.42 fof(f209,plain,(
% 0.12/0.42 genls(c_tptpcol_10_26886,c_tptpcol_9_26885)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f23])).
% 0.12/0.42 fof(f212,plain,(
% 0.12/0.42 genls(c_tptpcol_11_26887,c_tptpcol_10_26886)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f25])).
% 0.12/0.42 fof(f215,plain,(
% 0.12/0.42 genls(c_tptpcol_12_26919,c_tptpcol_11_26887)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f27])).
% 0.12/0.42 fof(f218,plain,(
% 0.12/0.42 genls(c_tptpcol_13_26920,c_tptpcol_12_26919)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f29])).
% 0.12/0.42 fof(f221,plain,(
% 0.12/0.42 genls(c_tptpcol_14_26921,c_tptpcol_13_26920)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f31])).
% 0.12/0.42 fof(f224,plain,(
% 0.12/0.42 genls(c_tptpcol_15_26925,c_tptpcol_14_26921)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f33])).
% 0.12/0.42 fof(f227,plain,(
% 0.12/0.42 genls(c_tptpcol_16_26926,c_tptpcol_15_26925)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f35])).
% 0.12/0.42 fof(f230,plain,(
% 0.12/0.42 genls(c_tptpcol_2_65537,c_tptpcol_1_65536)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f37])).
% 0.12/0.42 fof(f233,plain,(
% 0.12/0.42 genls(c_tptpcol_3_81921,c_tptpcol_2_65537)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f39])).
% 0.12/0.42 fof(f236,plain,(
% 0.12/0.42 genls(c_tptpcol_4_90113,c_tptpcol_3_81921)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f41])).
% 0.12/0.42 fof(f239,plain,(
% 0.12/0.42 genls(c_tptpcol_5_90114,c_tptpcol_4_90113)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f43])).
% 0.12/0.42 fof(f242,plain,(
% 0.12/0.42 genls(c_tptpcol_6_92162,c_tptpcol_5_90114)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f45])).
% 0.12/0.42 fof(f245,plain,(
% 0.12/0.42 genls(c_tptpcol_7_92163,c_tptpcol_6_92162)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f47])).
% 0.12/0.42 fof(f248,plain,(
% 0.12/0.42 genls(c_tptpcol_8_92164,c_tptpcol_7_92163)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f49])).
% 0.12/0.42 fof(f251,plain,(
% 0.12/0.42 genls(c_tptpcol_9_92165,c_tptpcol_8_92164)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f51])).
% 0.12/0.42 fof(f254,plain,(
% 0.12/0.42 genls(c_tptpcol_10_92166,c_tptpcol_9_92165)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f53])).
% 0.12/0.42 fof(f257,plain,(
% 0.12/0.42 genls(c_tptpcol_11_92230,c_tptpcol_10_92166)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f55])).
% 0.12/0.42 fof(f260,plain,(
% 0.12/0.42 genls(c_tptpcol_12_92262,c_tptpcol_11_92230)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f57])).
% 0.12/0.42 fof(f263,plain,(
% 0.12/0.42 genls(c_tptpcol_13_92263,c_tptpcol_12_92262)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f59])).
% 0.12/0.42 fof(f266,plain,(
% 0.12/0.42 genls(c_tptpcol_14_92264,c_tptpcol_13_92263)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f61])).
% 0.12/0.42 fof(f269,plain,(
% 0.12/0.42 genls(c_tptpcol_15_92268,c_tptpcol_14_92264)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f63])).
% 0.12/0.42 fof(f272,plain,(
% 0.12/0.42 genls(c_tptpcol_16_92269,c_tptpcol_15_92268)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f65])).
% 0.12/0.42 fof(f275,plain,(
% 0.12/0.42 disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f67])).
% 0.12/0.42 fof(f323,plain,(
% 0.12/0.42 ![ARG1,OLD,NEW]: ((~disjointwith(ARG1,OLD)|~genls(NEW,OLD))|disjointwith(ARG1,NEW))),
% 0.12/0.42 inference(pre_NNF_transformation,[status(thm)],[f85])).
% 0.12/0.42 fof(f324,plain,(
% 0.12/0.42 ![ARG1,NEW]: ((![OLD]: (~disjointwith(ARG1,OLD)|~genls(NEW,OLD)))|disjointwith(ARG1,NEW))),
% 0.12/0.42 inference(miniscoping,[status(thm)],[f323])).
% 0.12/0.42 fof(f325,plain,(
% 0.12/0.42 ![X0,X1,X2]: (~disjointwith(X0,X1)|~genls(X2,X1)|disjointwith(X0,X2))),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f324])).
% 0.12/0.42 fof(f326,plain,(
% 0.12/0.42 ![OLD,ARG2,NEW]: ((~disjointwith(OLD,ARG2)|~genls(NEW,OLD))|disjointwith(NEW,ARG2))),
% 0.12/0.42 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 0.12/0.42 fof(f327,plain,(
% 0.12/0.42 ![ARG2,NEW]: ((![OLD]: (~disjointwith(OLD,ARG2)|~genls(NEW,OLD)))|disjointwith(NEW,ARG2))),
% 0.12/0.42 inference(miniscoping,[status(thm)],[f326])).
% 0.12/0.42 fof(f328,plain,(
% 0.12/0.42 ![X0,X1,X2]: (~disjointwith(X0,X1)|~genls(X2,X0)|disjointwith(X2,X1))),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f327])).
% 0.12/0.42 fof(f469,plain,(
% 0.12/0.42 ![X,Y,Z]: ((~genls(X,Y)|~genls(Y,Z))|genls(X,Z))),
% 0.12/0.42 inference(pre_NNF_transformation,[status(thm)],[f155])).
% 0.12/0.42 fof(f470,plain,(
% 0.12/0.42 ![X,Z]: ((![Y]: (~genls(X,Y)|~genls(Y,Z)))|genls(X,Z))),
% 0.12/0.42 inference(miniscoping,[status(thm)],[f469])).
% 0.12/0.42 fof(f471,plain,(
% 0.12/0.42 ![X0,X1,X2]: (~genls(X0,X1)|~genls(X1,X2)|genls(X0,X2))),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f470])).
% 0.12/0.42 fof(f525,plain,(
% 0.12/0.42 (mtvisible(c_unitedstatesgeographypeoplemt)&~disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269))),
% 0.12/0.42 inference(pre_NNF_transformation,[status(thm)],[f178])).
% 0.12/0.42 fof(f527,plain,(
% 0.12/0.42 ~disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f525])).
% 0.12/0.42 fof(f539,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_1_1)|disjointwith(X0,c_tptpcol_1_65536))),
% 0.12/0.42 inference(resolution,[status(thm)],[f275,f328])).
% 0.12/0.42 fof(f550,plain,(
% 0.12/0.42 disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536)),
% 0.12/0.42 inference(resolution,[status(thm)],[f539,f185])).
% 0.12/0.42 fof(f556,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_2_2)|disjointwith(X0,c_tptpcol_1_65536))),
% 0.12/0.42 inference(resolution,[status(thm)],[f550,f328])).
% 0.12/0.42 fof(f574,plain,(
% 0.12/0.42 disjointwith(c_tptpcol_3_16386,c_tptpcol_1_65536)),
% 0.12/0.42 inference(resolution,[status(thm)],[f556,f188])).
% 0.12/0.42 fof(f580,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_3_16386)|disjointwith(X0,c_tptpcol_1_65536))),
% 0.12/0.42 inference(resolution,[status(thm)],[f574,f328])).
% 0.12/0.42 fof(f597,plain,(
% 0.12/0.42 disjointwith(c_tptpcol_4_24578,c_tptpcol_1_65536)),
% 0.12/0.42 inference(resolution,[status(thm)],[f580,f191])).
% 0.12/0.42 fof(f620,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_4_24578)|disjointwith(X0,c_tptpcol_1_65536))),
% 0.12/0.42 inference(resolution,[status(thm)],[f597,f328])).
% 0.12/0.42 fof(f655,plain,(
% 0.12/0.42 disjointwith(c_tptpcol_5_24579,c_tptpcol_1_65536)),
% 0.12/0.42 inference(resolution,[status(thm)],[f620,f194])).
% 0.12/0.42 fof(f675,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_1_65536)|disjointwith(c_tptpcol_5_24579,X0))),
% 0.12/0.42 inference(resolution,[status(thm)],[f655,f325])).
% 0.12/0.42 fof(f717,plain,(
% 0.12/0.42 disjointwith(c_tptpcol_5_24579,c_tptpcol_2_65537)),
% 0.12/0.42 inference(resolution,[status(thm)],[f675,f230])).
% 0.12/0.42 fof(f749,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_5_24579)|disjointwith(X0,c_tptpcol_2_65537))),
% 0.12/0.42 inference(resolution,[status(thm)],[f717,f328])).
% 0.12/0.42 fof(f837,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_15_92268)|genls(X0,c_tptpcol_14_92264))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f269])).
% 0.12/0.42 fof(f838,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_14_92264)|genls(X0,c_tptpcol_13_92263))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f266])).
% 0.12/0.42 fof(f839,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_13_92263)|genls(X0,c_tptpcol_12_92262))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f263])).
% 0.12/0.42 fof(f840,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_12_92262)|genls(X0,c_tptpcol_11_92230))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f260])).
% 0.12/0.42 fof(f841,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_11_92230)|genls(X0,c_tptpcol_10_92166))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f257])).
% 0.12/0.42 fof(f842,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_10_92166)|genls(X0,c_tptpcol_9_92165))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f254])).
% 0.12/0.42 fof(f843,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_9_92165)|genls(X0,c_tptpcol_8_92164))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f251])).
% 0.12/0.42 fof(f844,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_8_92164)|genls(X0,c_tptpcol_7_92163))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f248])).
% 0.12/0.42 fof(f845,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_7_92163)|genls(X0,c_tptpcol_6_92162))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f245])).
% 0.12/0.42 fof(f846,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_6_92162)|genls(X0,c_tptpcol_5_90114))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f242])).
% 0.12/0.42 fof(f847,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_5_90114)|genls(X0,c_tptpcol_4_90113))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f239])).
% 0.12/0.42 fof(f848,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_4_90113)|genls(X0,c_tptpcol_3_81921))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f236])).
% 0.12/0.42 fof(f849,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_3_81921)|genls(X0,c_tptpcol_2_65537))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f233])).
% 0.12/0.42 fof(f851,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_15_26925)|genls(X0,c_tptpcol_14_26921))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f224])).
% 0.12/0.42 fof(f852,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_14_26921)|genls(X0,c_tptpcol_13_26920))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f221])).
% 0.12/0.42 fof(f853,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_13_26920)|genls(X0,c_tptpcol_12_26919))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f218])).
% 0.12/0.42 fof(f854,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_12_26919)|genls(X0,c_tptpcol_11_26887))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f215])).
% 0.12/0.42 fof(f855,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_11_26887)|genls(X0,c_tptpcol_10_26886))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f212])).
% 0.12/0.42 fof(f856,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_10_26886)|genls(X0,c_tptpcol_9_26885))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f209])).
% 0.12/0.42 fof(f857,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_9_26885)|genls(X0,c_tptpcol_8_26629))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f206])).
% 0.12/0.42 fof(f858,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_8_26629)|genls(X0,c_tptpcol_7_26628))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f203])).
% 0.12/0.42 fof(f859,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_7_26628)|genls(X0,c_tptpcol_6_26627))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f200])).
% 0.12/0.42 fof(f860,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_6_26627)|genls(X0,c_tptpcol_5_24579))),
% 0.12/0.42 inference(resolution,[status(thm)],[f471,f197])).
% 0.12/0.42 fof(f1096,plain,(
% 0.12/0.42 genls(c_tptpcol_16_92269,c_tptpcol_14_92264)),
% 0.12/0.42 inference(resolution,[status(thm)],[f837,f272])).
% 0.12/0.42 fof(f1107,plain,(
% 0.12/0.42 genls(c_tptpcol_16_92269,c_tptpcol_13_92263)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1096,f838])).
% 0.12/0.42 fof(f1111,plain,(
% 0.12/0.42 genls(c_tptpcol_16_92269,c_tptpcol_12_92262)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1107,f839])).
% 0.12/0.42 fof(f1121,plain,(
% 0.12/0.42 genls(c_tptpcol_16_92269,c_tptpcol_11_92230)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1111,f840])).
% 0.12/0.42 fof(f1126,plain,(
% 0.12/0.42 genls(c_tptpcol_16_92269,c_tptpcol_10_92166)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1121,f841])).
% 0.12/0.42 fof(f1148,plain,(
% 0.12/0.42 genls(c_tptpcol_16_92269,c_tptpcol_9_92165)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1126,f842])).
% 0.12/0.42 fof(f1158,plain,(
% 0.12/0.42 genls(c_tptpcol_16_92269,c_tptpcol_8_92164)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1148,f843])).
% 0.12/0.42 fof(f1163,plain,(
% 0.12/0.42 genls(c_tptpcol_16_92269,c_tptpcol_7_92163)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1158,f844])).
% 0.12/0.42 fof(f1173,plain,(
% 0.12/0.42 genls(c_tptpcol_16_26926,c_tptpcol_14_26921)),
% 0.12/0.42 inference(resolution,[status(thm)],[f851,f227])).
% 0.12/0.42 fof(f1177,plain,(
% 0.12/0.42 genls(c_tptpcol_16_26926,c_tptpcol_13_26920)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1173,f852])).
% 0.12/0.42 fof(f1181,plain,(
% 0.12/0.42 genls(c_tptpcol_16_26926,c_tptpcol_12_26919)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1177,f853])).
% 0.12/0.42 fof(f1191,plain,(
% 0.12/0.42 genls(c_tptpcol_16_26926,c_tptpcol_11_26887)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1181,f854])).
% 0.12/0.42 fof(f1204,plain,(
% 0.12/0.42 genls(c_tptpcol_16_26926,c_tptpcol_10_26886)),
% 0.12/0.42 inference(resolution,[status(thm)],[f855,f1191])).
% 0.12/0.42 fof(f1223,plain,(
% 0.12/0.42 genls(c_tptpcol_16_26926,c_tptpcol_9_26885)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1204,f856])).
% 0.12/0.42 fof(f1227,plain,(
% 0.12/0.42 genls(c_tptpcol_16_26926,c_tptpcol_8_26629)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1223,f857])).
% 0.12/0.42 fof(f1280,plain,(
% 0.12/0.42 genls(c_tptpcol_16_26926,c_tptpcol_7_26628)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1227,f858])).
% 0.12/0.42 fof(f1285,plain,(
% 0.12/0.42 genls(c_tptpcol_16_92269,c_tptpcol_6_92162)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1163,f845])).
% 0.12/0.42 fof(f1384,plain,(
% 0.12/0.42 genls(c_tptpcol_16_26926,c_tptpcol_6_26627)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1280,f859])).
% 0.12/0.42 fof(f1388,plain,(
% 0.12/0.42 genls(c_tptpcol_16_92269,c_tptpcol_5_90114)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1285,f846])).
% 0.12/0.42 fof(f1393,plain,(
% 0.12/0.42 genls(c_tptpcol_16_26926,c_tptpcol_5_24579)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1384,f860])).
% 0.12/0.42 fof(f1401,plain,(
% 0.12/0.42 genls(c_tptpcol_16_92269,c_tptpcol_4_90113)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1388,f847])).
% 0.12/0.42 fof(f1453,plain,(
% 0.12/0.42 disjointwith(c_tptpcol_16_26926,c_tptpcol_2_65537)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1393,f749])).
% 0.12/0.42 fof(f1464,plain,(
% 0.12/0.42 genls(c_tptpcol_16_92269,c_tptpcol_3_81921)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1401,f848])).
% 0.12/0.42 fof(f1658,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_2_65537)|disjointwith(c_tptpcol_16_26926,X0))),
% 0.12/0.42 inference(resolution,[status(thm)],[f1453,f325])).
% 0.12/0.42 fof(f1728,plain,(
% 0.12/0.42 genls(c_tptpcol_16_92269,c_tptpcol_2_65537)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1464,f849])).
% 0.12/0.42 fof(f2423,plain,(
% 0.12/0.42 disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1658,f1728])).
% 0.12/0.42 fof(f2424,plain,(
% 0.12/0.42 $false),
% 0.12/0.42 inference(forward_subsumption_resolution,[status(thm)],[f2423,f527])).
% 0.12/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.44 % Elapsed time: 0.073717 seconds
% 0.12/0.44 % CPU time: 0.337882 seconds
% 0.12/0.44 % Total memory used: 48.770 MB
% 0.12/0.44 % Net memory used: 48.356 MB
%------------------------------------------------------------------------------