%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR039+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:43 PM UTC 2026
% Result : Theorem 0.12s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR039+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n010.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 21 14:30:25 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 0.12/0.43 % Refutation found
% 0.12/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.43 fof(f7,axiom,(
% 0.12/0.43 genls(c_tptpcol_2_2,c_tptpcol_1_1) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f9,axiom,(
% 0.12/0.43 genls(c_tptpcol_3_16386,c_tptpcol_2_2) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f11,axiom,(
% 0.12/0.43 genls(c_tptpcol_4_16387,c_tptpcol_3_16386) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f13,axiom,(
% 0.12/0.43 genls(c_tptpcol_5_16388,c_tptpcol_4_16387) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f15,axiom,(
% 0.12/0.43 genls(c_tptpcol_6_18436,c_tptpcol_5_16388) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f17,axiom,(
% 0.12/0.43 genls(c_tptpcol_7_18437,c_tptpcol_6_18436) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f19,axiom,(
% 0.12/0.43 genls(c_tptpcol_8_18438,c_tptpcol_7_18437) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f21,axiom,(
% 0.12/0.43 genls(c_tptpcol_9_18439,c_tptpcol_8_18438) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f23,axiom,(
% 0.12/0.43 genls(c_tptpcol_10_18567,c_tptpcol_9_18439) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f25,axiom,(
% 0.12/0.43 genls(c_tptpcol_11_18631,c_tptpcol_10_18567) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f27,axiom,(
% 0.12/0.43 genls(c_tptpcol_12_18663,c_tptpcol_11_18631) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f29,axiom,(
% 0.12/0.43 genls(c_tptpcol_13_18664,c_tptpcol_12_18663) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f31,axiom,(
% 0.12/0.43 genls(c_tptpcol_2_65537,c_tptpcol_1_65536) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f33,axiom,(
% 0.12/0.43 genls(c_tptpcol_3_81921,c_tptpcol_2_65537) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f35,axiom,(
% 0.12/0.43 genls(c_tptpcol_4_90113,c_tptpcol_3_81921) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f37,axiom,(
% 0.12/0.43 genls(c_tptpcol_5_90114,c_tptpcol_4_90113) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f39,axiom,(
% 0.12/0.43 genls(c_tptpcol_6_92162,c_tptpcol_5_90114) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f41,axiom,(
% 0.12/0.43 genls(c_tptpcol_7_93186,c_tptpcol_6_92162) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f43,axiom,(
% 0.12/0.43 genls(c_tptpcol_8_93698,c_tptpcol_7_93186) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f45,axiom,(
% 0.12/0.43 genls(c_tptpcol_9_93699,c_tptpcol_8_93698) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f47,axiom,(
% 0.12/0.43 genls(c_tptpcol_10_93700,c_tptpcol_9_93699) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f49,axiom,(
% 0.12/0.43 genls(c_tptpcol_11_93764,c_tptpcol_10_93700) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f51,axiom,(
% 0.12/0.43 genls(c_tptpcol_12_93765,c_tptpcol_11_93764) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f53,axiom,(
% 0.12/0.43 genls(c_tptpcol_13_93766,c_tptpcol_12_93765) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f55,axiom,(
% 0.12/0.43 genls(c_tptpcol_14_93774,c_tptpcol_13_93766) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f57,axiom,(
% 0.12/0.43 genls(c_tptpcol_15_93775,c_tptpcol_14_93774) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f59,axiom,(
% 0.12/0.43 disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f76,axiom,(
% 0.12/0.43 (! [X,Y] :( disjointwith(X,Y)=> disjointwith(Y,X) ) )),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f77,axiom,(
% 0.12/0.43 (! [ARG1,OLD,NEW] :( ( disjointwith(ARG1,OLD)& genls(NEW,OLD) )=> disjointwith(ARG1,NEW) ) )),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f78,axiom,(
% 0.12/0.43 (! [OLD,ARG2,NEW] :( ( disjointwith(OLD,ARG2)& genls(NEW,OLD) )=> disjointwith(NEW,ARG2) ) )),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f139,axiom,(
% 0.12/0.43 (! [X,Y,Z] :( ( genls(X,Y)& genls(Y,Z) )=> genls(X,Z) ) )),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f171,conjecture,(
% 0.12/0.43 ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))=> disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f172,negated_conjecture,(
% 0.12/0.43 ~(( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))=> disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ) )),
% 0.12/0.43 inference(negated_conjecture,[status(cth)],[f171])).
% 0.12/0.43 fof(f179,plain,(
% 0.12/0.43 genls(c_tptpcol_2_2,c_tptpcol_1_1)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.43 fof(f182,plain,(
% 0.12/0.43 genls(c_tptpcol_3_16386,c_tptpcol_2_2)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f9])).
% 0.12/0.43 fof(f185,plain,(
% 0.12/0.43 genls(c_tptpcol_4_16387,c_tptpcol_3_16386)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f11])).
% 0.12/0.43 fof(f188,plain,(
% 0.12/0.43 genls(c_tptpcol_5_16388,c_tptpcol_4_16387)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f13])).
% 0.12/0.43 fof(f191,plain,(
% 0.12/0.43 genls(c_tptpcol_6_18436,c_tptpcol_5_16388)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f15])).
% 0.12/0.43 fof(f194,plain,(
% 0.12/0.43 genls(c_tptpcol_7_18437,c_tptpcol_6_18436)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f17])).
% 0.12/0.43 fof(f197,plain,(
% 0.12/0.43 genls(c_tptpcol_8_18438,c_tptpcol_7_18437)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f19])).
% 0.12/0.43 fof(f200,plain,(
% 0.12/0.43 genls(c_tptpcol_9_18439,c_tptpcol_8_18438)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f21])).
% 0.12/0.43 fof(f203,plain,(
% 0.12/0.43 genls(c_tptpcol_10_18567,c_tptpcol_9_18439)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f23])).
% 0.12/0.43 fof(f206,plain,(
% 0.12/0.43 genls(c_tptpcol_11_18631,c_tptpcol_10_18567)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f25])).
% 0.12/0.43 fof(f209,plain,(
% 0.12/0.43 genls(c_tptpcol_12_18663,c_tptpcol_11_18631)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f27])).
% 0.12/0.43 fof(f212,plain,(
% 0.12/0.43 genls(c_tptpcol_13_18664,c_tptpcol_12_18663)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f29])).
% 0.12/0.43 fof(f215,plain,(
% 0.12/0.43 genls(c_tptpcol_2_65537,c_tptpcol_1_65536)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f31])).
% 0.12/0.43 fof(f218,plain,(
% 0.12/0.43 genls(c_tptpcol_3_81921,c_tptpcol_2_65537)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f33])).
% 0.12/0.43 fof(f221,plain,(
% 0.12/0.43 genls(c_tptpcol_4_90113,c_tptpcol_3_81921)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f35])).
% 0.12/0.43 fof(f224,plain,(
% 0.12/0.43 genls(c_tptpcol_5_90114,c_tptpcol_4_90113)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f37])).
% 0.12/0.43 fof(f227,plain,(
% 0.12/0.43 genls(c_tptpcol_6_92162,c_tptpcol_5_90114)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f39])).
% 0.12/0.43 fof(f230,plain,(
% 0.12/0.43 genls(c_tptpcol_7_93186,c_tptpcol_6_92162)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f41])).
% 0.12/0.43 fof(f233,plain,(
% 0.12/0.43 genls(c_tptpcol_8_93698,c_tptpcol_7_93186)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f43])).
% 0.12/0.43 fof(f236,plain,(
% 0.12/0.43 genls(c_tptpcol_9_93699,c_tptpcol_8_93698)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f45])).
% 0.12/0.43 fof(f239,plain,(
% 0.12/0.43 genls(c_tptpcol_10_93700,c_tptpcol_9_93699)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f47])).
% 0.12/0.43 fof(f242,plain,(
% 0.12/0.43 genls(c_tptpcol_11_93764,c_tptpcol_10_93700)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f49])).
% 0.12/0.43 fof(f245,plain,(
% 0.12/0.43 genls(c_tptpcol_12_93765,c_tptpcol_11_93764)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f51])).
% 0.12/0.43 fof(f248,plain,(
% 0.12/0.43 genls(c_tptpcol_13_93766,c_tptpcol_12_93765)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f53])).
% 0.12/0.43 fof(f251,plain,(
% 0.12/0.43 genls(c_tptpcol_14_93774,c_tptpcol_13_93766)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f55])).
% 0.12/0.43 fof(f254,plain,(
% 0.12/0.43 genls(c_tptpcol_15_93775,c_tptpcol_14_93774)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f57])).
% 0.12/0.43 fof(f257,plain,(
% 0.12/0.43 disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f59])).
% 0.12/0.43 fof(f303,plain,(
% 0.12/0.43 ![X,Y]: (~disjointwith(X,Y)|disjointwith(Y,X))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f76])).
% 0.12/0.43 fof(f304,plain,(
% 0.12/0.43 ![X0,X1]: (~disjointwith(X0,X1)|disjointwith(X1,X0))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f303])).
% 0.12/0.43 fof(f305,plain,(
% 0.12/0.43 ![ARG1,OLD,NEW]: ((~disjointwith(ARG1,OLD)|~genls(NEW,OLD))|disjointwith(ARG1,NEW))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f77])).
% 0.12/0.43 fof(f306,plain,(
% 0.12/0.43 ![ARG1,NEW]: ((![OLD]: (~disjointwith(ARG1,OLD)|~genls(NEW,OLD)))|disjointwith(ARG1,NEW))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f305])).
% 0.12/0.43 fof(f307,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~disjointwith(X0,X1)|~genls(X2,X1)|disjointwith(X0,X2))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f306])).
% 0.12/0.43 fof(f308,plain,(
% 0.12/0.43 ![OLD,ARG2,NEW]: ((~disjointwith(OLD,ARG2)|~genls(NEW,OLD))|disjointwith(NEW,ARG2))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f78])).
% 0.12/0.43 fof(f309,plain,(
% 0.12/0.43 ![ARG2,NEW]: ((![OLD]: (~disjointwith(OLD,ARG2)|~genls(NEW,OLD)))|disjointwith(NEW,ARG2))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f308])).
% 0.12/0.43 fof(f310,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~disjointwith(X0,X1)|~genls(X2,X0)|disjointwith(X2,X1))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f309])).
% 0.12/0.43 fof(f435,plain,(
% 0.12/0.43 ![X,Y,Z]: ((~genls(X,Y)|~genls(Y,Z))|genls(X,Z))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f139])).
% 0.12/0.43 fof(f436,plain,(
% 0.12/0.43 ![X,Z]: ((![Y]: (~genls(X,Y)|~genls(Y,Z)))|genls(X,Z))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f435])).
% 0.12/0.43 fof(f437,plain,(
% 0.12/0.43 ![X0,X1,X2]: (~genls(X0,X1)|~genls(X1,X2)|genls(X0,X2))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f436])).
% 0.12/0.43 fof(f501,plain,(
% 0.12/0.43 (mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))&~disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664))),
% 0.12/0.43 inference(pre_NNF_transformation,[status(thm)],[f172])).
% 0.12/0.43 fof(f503,plain,(
% 0.12/0.43 ~disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f501])).
% 0.12/0.43 fof(f515,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_1_1)|disjointwith(X0,c_tptpcol_1_65536))),
% 0.12/0.43 inference(resolution,[status(thm)],[f257,f310])).
% 0.12/0.43 fof(f518,plain,(
% 0.12/0.43 disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536)),
% 0.12/0.43 inference(resolution,[status(thm)],[f515,f179])).
% 0.12/0.43 fof(f523,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_2_2)|disjointwith(X0,c_tptpcol_1_65536))),
% 0.12/0.43 inference(resolution,[status(thm)],[f518,f310])).
% 0.12/0.43 fof(f540,plain,(
% 0.12/0.43 disjointwith(c_tptpcol_3_16386,c_tptpcol_1_65536)),
% 0.12/0.43 inference(resolution,[status(thm)],[f523,f182])).
% 0.12/0.43 fof(f556,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_3_16386)|disjointwith(X0,c_tptpcol_1_65536))),
% 0.12/0.43 inference(resolution,[status(thm)],[f540,f310])).
% 0.12/0.43 fof(f583,plain,(
% 0.12/0.43 disjointwith(c_tptpcol_4_16387,c_tptpcol_1_65536)),
% 0.12/0.43 inference(resolution,[status(thm)],[f556,f185])).
% 0.12/0.43 fof(f591,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_4_16387)|disjointwith(X0,c_tptpcol_1_65536))),
% 0.12/0.43 inference(resolution,[status(thm)],[f583,f310])).
% 0.12/0.43 fof(f641,plain,(
% 0.12/0.43 disjointwith(c_tptpcol_5_16388,c_tptpcol_1_65536)),
% 0.12/0.43 inference(resolution,[status(thm)],[f591,f188])).
% 0.12/0.43 fof(f647,plain,(
% 0.12/0.43 disjointwith(c_tptpcol_1_65536,c_tptpcol_5_16388)),
% 0.12/0.43 inference(resolution,[status(thm)],[f641,f304])).
% 0.12/0.43 fof(f660,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_5_16388)|disjointwith(c_tptpcol_1_65536,X0))),
% 0.12/0.43 inference(resolution,[status(thm)],[f647,f307])).
% 0.12/0.43 fof(f836,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_14_93774)|genls(X0,c_tptpcol_13_93766))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f251])).
% 0.12/0.43 fof(f837,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_13_93766)|genls(X0,c_tptpcol_12_93765))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f248])).
% 0.12/0.43 fof(f838,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_12_93765)|genls(X0,c_tptpcol_11_93764))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f245])).
% 0.12/0.43 fof(f839,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_11_93764)|genls(X0,c_tptpcol_10_93700))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f242])).
% 0.12/0.43 fof(f840,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_10_93700)|genls(X0,c_tptpcol_9_93699))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f239])).
% 0.12/0.43 fof(f841,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_9_93699)|genls(X0,c_tptpcol_8_93698))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f236])).
% 0.12/0.43 fof(f842,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_8_93698)|genls(X0,c_tptpcol_7_93186))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f233])).
% 0.12/0.43 fof(f843,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_7_93186)|genls(X0,c_tptpcol_6_92162))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f230])).
% 0.12/0.43 fof(f844,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_6_92162)|genls(X0,c_tptpcol_5_90114))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f227])).
% 0.12/0.43 fof(f845,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_5_90114)|genls(X0,c_tptpcol_4_90113))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f224])).
% 0.12/0.43 fof(f846,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_4_90113)|genls(X0,c_tptpcol_3_81921))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f221])).
% 0.12/0.43 fof(f847,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_3_81921)|genls(X0,c_tptpcol_2_65537))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f218])).
% 0.12/0.43 fof(f848,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_2_65537)|genls(X0,c_tptpcol_1_65536))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f215])).
% 0.12/0.43 fof(f849,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_12_18663)|genls(X0,c_tptpcol_11_18631))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f209])).
% 0.12/0.43 fof(f850,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_11_18631)|genls(X0,c_tptpcol_10_18567))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f206])).
% 0.12/0.43 fof(f851,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_10_18567)|genls(X0,c_tptpcol_9_18439))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f203])).
% 0.12/0.43 fof(f852,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_9_18439)|genls(X0,c_tptpcol_8_18438))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f200])).
% 0.12/0.43 fof(f853,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_8_18438)|genls(X0,c_tptpcol_7_18437))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f197])).
% 0.12/0.43 fof(f854,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_7_18437)|genls(X0,c_tptpcol_6_18436))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f194])).
% 0.12/0.43 fof(f855,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_6_18436)|genls(X0,c_tptpcol_5_16388))),
% 0.12/0.43 inference(resolution,[status(thm)],[f437,f191])).
% 0.12/0.43 fof(f1047,plain,(
% 0.12/0.43 genls(c_tptpcol_15_93775,c_tptpcol_13_93766)),
% 0.12/0.43 inference(resolution,[status(thm)],[f836,f254])).
% 0.12/0.43 fof(f1057,plain,(
% 0.12/0.43 genls(c_tptpcol_15_93775,c_tptpcol_12_93765)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1047,f837])).
% 0.12/0.43 fof(f1061,plain,(
% 0.12/0.43 genls(c_tptpcol_15_93775,c_tptpcol_11_93764)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1057,f838])).
% 0.12/0.43 fof(f1076,plain,(
% 0.12/0.43 genls(c_tptpcol_15_93775,c_tptpcol_10_93700)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1061,f839])).
% 0.12/0.43 fof(f1081,plain,(
% 0.12/0.43 genls(c_tptpcol_15_93775,c_tptpcol_9_93699)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1076,f840])).
% 0.12/0.43 fof(f1103,plain,(
% 0.12/0.43 genls(c_tptpcol_15_93775,c_tptpcol_8_93698)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1081,f841])).
% 0.12/0.43 fof(f1112,plain,(
% 0.12/0.43 genls(c_tptpcol_15_93775,c_tptpcol_7_93186)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1103,f842])).
% 0.12/0.43 fof(f1118,plain,(
% 0.12/0.43 genls(c_tptpcol_15_93775,c_tptpcol_6_92162)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1112,f843])).
% 0.12/0.43 fof(f1137,plain,(
% 0.12/0.43 genls(c_tptpcol_13_18664,c_tptpcol_11_18631)),
% 0.12/0.43 inference(resolution,[status(thm)],[f849,f212])).
% 0.12/0.43 fof(f1141,plain,(
% 0.12/0.43 genls(c_tptpcol_15_93775,c_tptpcol_5_90114)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1118,f844])).
% 0.12/0.43 fof(f1145,plain,(
% 0.12/0.43 genls(c_tptpcol_13_18664,c_tptpcol_10_18567)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1137,f850])).
% 0.12/0.43 fof(f1149,plain,(
% 0.12/0.43 genls(c_tptpcol_13_18664,c_tptpcol_9_18439)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1145,f851])).
% 0.12/0.43 fof(f1153,plain,(
% 0.12/0.43 genls(c_tptpcol_15_93775,c_tptpcol_4_90113)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1141,f845])).
% 0.12/0.43 fof(f1159,plain,(
% 0.12/0.43 genls(c_tptpcol_13_18664,c_tptpcol_8_18438)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1149,f852])).
% 0.12/0.43 fof(f1182,plain,(
% 0.12/0.43 genls(c_tptpcol_13_18664,c_tptpcol_7_18437)),
% 0.12/0.43 inference(resolution,[status(thm)],[f853,f1159])).
% 0.12/0.43 fof(f1192,plain,(
% 0.12/0.43 genls(c_tptpcol_15_93775,c_tptpcol_3_81921)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1153,f846])).
% 0.12/0.43 fof(f1201,plain,(
% 0.12/0.43 genls(c_tptpcol_13_18664,c_tptpcol_6_18436)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1182,f854])).
% 0.12/0.43 fof(f1215,plain,(
% 0.12/0.43 genls(c_tptpcol_13_18664,c_tptpcol_5_16388)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1201,f855])).
% 0.12/0.43 fof(f1223,plain,(
% 0.12/0.43 disjointwith(c_tptpcol_1_65536,c_tptpcol_13_18664)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1215,f660])).
% 0.12/0.43 fof(f1249,plain,(
% 0.12/0.43 genls(c_tptpcol_15_93775,c_tptpcol_2_65537)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1192,f847])).
% 0.12/0.44 fof(f1393,plain,(
% 0.12/0.44 ![X0]: (~genls(X0,c_tptpcol_1_65536)|disjointwith(X0,c_tptpcol_13_18664))),
% 0.12/0.44 inference(resolution,[status(thm)],[f1223,f310])).
% 0.12/0.44 fof(f1407,plain,(
% 0.12/0.44 genls(c_tptpcol_15_93775,c_tptpcol_1_65536)),
% 0.12/0.44 inference(resolution,[status(thm)],[f1249,f848])).
% 0.12/0.44 fof(f2103,plain,(
% 0.12/0.44 disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664)),
% 0.12/0.44 inference(resolution,[status(thm)],[f1393,f1407])).
% 0.12/0.44 fof(f2104,plain,(
% 0.12/0.44 $false),
% 0.12/0.44 inference(forward_subsumption_resolution,[status(thm)],[f2103,f503])).
% 0.12/0.44 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.45 % Elapsed time: 0.076626 seconds
% 0.12/0.45 % CPU time: 0.371858 seconds
% 0.12/0.45 % Total memory used: 68.276 MB
% 0.12/0.45 % Net memory used: 67.686 MB
%------------------------------------------------------------------------------