%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR039+2 : 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 : n003.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.92s 0.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR039+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n003.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 14:31:46 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.92/0.69 % Refutation found
% 0.92/0.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.92/0.69 % SZS output start CNFRefutation for theBenchmark
% 0.92/0.69 fof(f14,axiom,(
% 0.92/0.69 genls(c_tptpcol_7_93186,c_tptpcol_6_92162) ),
% 0.92/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.69 fof(f23,axiom,(
% 0.92/0.69 genls(c_tptpcol_5_16388,c_tptpcol_4_16387) ),
% 0.92/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.69 fof(f41,axiom,(
% 0.92/0.69 genls(c_tptpcol_3_81921,c_tptpcol_2_65537) ),
% 0.92/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.69 fof(f43,axiom,(
% 0.92/0.69 genls(c_tptpcol_10_18567,c_tptpcol_9_18439) ),
% 0.92/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.69 fof(f72,axiom,(
% 0.92/0.69 genls(c_tptpcol_12_93765,c_tptpcol_11_93764) ),
% 0.92/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.69 fof(f78,axiom,(
% 0.92/0.69 genls(c_tptpcol_13_93766,c_tptpcol_12_93765) ),
% 0.92/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.69 fof(f109,axiom,(
% 0.92/0.69 genls(c_tptpcol_12_18663,c_tptpcol_11_18631) ),
% 0.92/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.69 fof(f145,axiom,(
% 0.92/0.70 genls(c_tptpcol_2_2,c_tptpcol_1_1) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f152,axiom,(
% 0.92/0.70 disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f175,axiom,(
% 0.92/0.70 genls(c_tptpcol_11_18631,c_tptpcol_10_18567) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f182,axiom,(
% 0.92/0.70 genls(c_tptpcol_15_93775,c_tptpcol_14_93774) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f191,axiom,(
% 0.92/0.70 genls(c_tptpcol_14_93774,c_tptpcol_13_93766) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f208,axiom,(
% 0.92/0.70 genls(c_tptpcol_13_18664,c_tptpcol_12_18663) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f255,axiom,(
% 0.92/0.70 genls(c_tptpcol_9_18439,c_tptpcol_8_18438) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f285,axiom,(
% 0.92/0.70 genls(c_tptpcol_4_16387,c_tptpcol_3_16386) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f345,axiom,(
% 0.92/0.70 genls(c_tptpcol_8_93698,c_tptpcol_7_93186) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f348,axiom,(
% 0.92/0.70 genls(c_tptpcol_2_65537,c_tptpcol_1_65536) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f351,axiom,(
% 0.92/0.70 genls(c_tptpcol_6_18436,c_tptpcol_5_16388) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f353,axiom,(
% 0.92/0.70 genls(c_tptpcol_8_18438,c_tptpcol_7_18437) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f370,axiom,(
% 0.92/0.70 genls(c_tptpcol_9_93699,c_tptpcol_8_93698) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f372,axiom,(
% 0.92/0.70 genls(c_tptpcol_11_93764,c_tptpcol_10_93700) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f376,axiom,(
% 0.92/0.70 genls(c_tptpcol_4_90113,c_tptpcol_3_81921) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f379,axiom,(
% 0.92/0.70 genls(c_tptpcol_10_93700,c_tptpcol_9_93699) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f385,axiom,(
% 0.92/0.70 genls(c_tptpcol_3_16386,c_tptpcol_2_2) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f417,axiom,(
% 0.92/0.70 genls(c_tptpcol_6_92162,c_tptpcol_5_90114) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f476,axiom,(
% 0.92/0.70 genls(c_tptpcol_5_90114,c_tptpcol_4_90113) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f483,axiom,(
% 0.92/0.70 genls(c_tptpcol_7_18437,c_tptpcol_6_18436) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f1120,axiom,(
% 0.92/0.70 (! [X,Y] :( disjointwith(X,Y)=> disjointwith(Y,X) ) )),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f1121,axiom,(
% 0.92/0.70 (! [ARG1,OLD,NEW] :( ( disjointwith(ARG1,OLD)& genls(NEW,OLD) )=> disjointwith(ARG1,NEW) ) )),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f1122,axiom,(
% 0.92/0.70 (! [OLD,ARG2,NEW] :( ( disjointwith(OLD,ARG2)& genls(NEW,OLD) )=> disjointwith(NEW,ARG2) ) )),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f1132,conjecture,(
% 0.92/0.70 ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))=> disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ) ),
% 0.92/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.92/0.70 fof(f1133,negated_conjecture,(
% 0.92/0.70 ~(( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))=> disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ) )),
% 0.92/0.70 inference(negated_conjecture,[status(cth)],[f1132])).
% 0.92/0.70 fof(f1154,plain,(
% 0.92/0.70 genls(c_tptpcol_7_93186,c_tptpcol_6_92162)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f14])).
% 0.92/0.70 fof(f1167,plain,(
% 0.92/0.70 genls(c_tptpcol_5_16388,c_tptpcol_4_16387)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f23])).
% 0.92/0.70 fof(f1194,plain,(
% 0.92/0.70 genls(c_tptpcol_3_81921,c_tptpcol_2_65537)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f41])).
% 0.92/0.70 fof(f1197,plain,(
% 0.92/0.70 genls(c_tptpcol_10_18567,c_tptpcol_9_18439)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f43])).
% 0.92/0.70 fof(f1237,plain,(
% 0.92/0.70 genls(c_tptpcol_12_93765,c_tptpcol_11_93764)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f72])).
% 0.92/0.70 fof(f1246,plain,(
% 0.92/0.70 genls(c_tptpcol_13_93766,c_tptpcol_12_93765)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f78])).
% 0.92/0.70 fof(f1292,plain,(
% 0.92/0.70 genls(c_tptpcol_12_18663,c_tptpcol_11_18631)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f109])).
% 0.92/0.70 fof(f1343,plain,(
% 0.92/0.70 genls(c_tptpcol_2_2,c_tptpcol_1_1)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f145])).
% 0.92/0.70 fof(f1353,plain,(
% 0.92/0.70 disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f152])).
% 0.92/0.70 fof(f1389,plain,(
% 0.92/0.70 genls(c_tptpcol_11_18631,c_tptpcol_10_18567)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f175])).
% 0.92/0.70 fof(f1399,plain,(
% 0.92/0.70 genls(c_tptpcol_15_93775,c_tptpcol_14_93774)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f182])).
% 0.92/0.70 fof(f1413,plain,(
% 0.92/0.70 genls(c_tptpcol_14_93774,c_tptpcol_13_93766)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f191])).
% 0.92/0.70 fof(f1438,plain,(
% 0.92/0.70 genls(c_tptpcol_13_18664,c_tptpcol_12_18663)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f208])).
% 0.92/0.70 fof(f1505,plain,(
% 0.92/0.70 genls(c_tptpcol_9_18439,c_tptpcol_8_18438)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f255])).
% 0.92/0.70 fof(f1548,plain,(
% 0.92/0.70 genls(c_tptpcol_4_16387,c_tptpcol_3_16386)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f285])).
% 0.92/0.70 fof(f1636,plain,(
% 0.92/0.70 genls(c_tptpcol_8_93698,c_tptpcol_7_93186)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f345])).
% 0.92/0.70 fof(f1640,plain,(
% 0.92/0.70 genls(c_tptpcol_2_65537,c_tptpcol_1_65536)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f348])).
% 0.92/0.70 fof(f1644,plain,(
% 0.92/0.70 genls(c_tptpcol_6_18436,c_tptpcol_5_16388)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f351])).
% 0.92/0.70 fof(f1647,plain,(
% 0.92/0.70 genls(c_tptpcol_8_18438,c_tptpcol_7_18437)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f353])).
% 0.92/0.70 fof(f1672,plain,(
% 0.92/0.70 genls(c_tptpcol_9_93699,c_tptpcol_8_93698)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f370])).
% 0.92/0.70 fof(f1675,plain,(
% 0.92/0.70 genls(c_tptpcol_11_93764,c_tptpcol_10_93700)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f372])).
% 0.92/0.70 fof(f1681,plain,(
% 0.92/0.70 genls(c_tptpcol_4_90113,c_tptpcol_3_81921)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f376])).
% 0.92/0.70 fof(f1685,plain,(
% 0.92/0.70 genls(c_tptpcol_10_93700,c_tptpcol_9_93699)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f379])).
% 0.92/0.70 fof(f1694,plain,(
% 0.92/0.70 genls(c_tptpcol_3_16386,c_tptpcol_2_2)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f385])).
% 0.92/0.70 fof(f1741,plain,(
% 0.92/0.70 genls(c_tptpcol_6_92162,c_tptpcol_5_90114)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f417])).
% 0.92/0.70 fof(f1829,plain,(
% 0.92/0.70 genls(c_tptpcol_5_90114,c_tptpcol_4_90113)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f476])).
% 0.92/0.70 fof(f1840,plain,(
% 0.92/0.70 genls(c_tptpcol_7_18437,c_tptpcol_6_18436)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f483])).
% 0.92/0.70 fof(f3173,plain,(
% 0.92/0.70 ![X,Y]: (~disjointwith(X,Y)|disjointwith(Y,X))),
% 0.92/0.70 inference(pre_NNF_transformation,[status(thm)],[f1120])).
% 0.92/0.70 fof(f3174,plain,(
% 0.92/0.70 ![X0,X1]: (~disjointwith(X0,X1)|disjointwith(X1,X0))),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f3173])).
% 0.92/0.70 fof(f3175,plain,(
% 0.92/0.70 ![ARG1,OLD,NEW]: ((~disjointwith(ARG1,OLD)|~genls(NEW,OLD))|disjointwith(ARG1,NEW))),
% 0.92/0.70 inference(pre_NNF_transformation,[status(thm)],[f1121])).
% 0.92/0.70 fof(f3176,plain,(
% 0.92/0.70 ![ARG1,NEW]: ((![OLD]: (~disjointwith(ARG1,OLD)|~genls(NEW,OLD)))|disjointwith(ARG1,NEW))),
% 0.92/0.70 inference(miniscoping,[status(thm)],[f3175])).
% 0.92/0.70 fof(f3177,plain,(
% 0.92/0.70 ![X0,X1,X2]: (~disjointwith(X0,X1)|~genls(X2,X1)|disjointwith(X0,X2))),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f3176])).
% 0.92/0.70 fof(f3178,plain,(
% 0.92/0.70 ![OLD,ARG2,NEW]: ((~disjointwith(OLD,ARG2)|~genls(NEW,OLD))|disjointwith(NEW,ARG2))),
% 0.92/0.70 inference(pre_NNF_transformation,[status(thm)],[f1122])).
% 0.92/0.70 fof(f3179,plain,(
% 0.92/0.70 ![ARG2,NEW]: ((![OLD]: (~disjointwith(OLD,ARG2)|~genls(NEW,OLD)))|disjointwith(NEW,ARG2))),
% 0.92/0.70 inference(miniscoping,[status(thm)],[f3178])).
% 0.92/0.70 fof(f3180,plain,(
% 0.92/0.70 ![X0,X1,X2]: (~disjointwith(X0,X1)|~genls(X2,X0)|disjointwith(X2,X1))),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f3179])).
% 0.92/0.70 fof(f3204,plain,(
% 0.92/0.70 (mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))&~disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664))),
% 0.92/0.70 inference(pre_NNF_transformation,[status(thm)],[f1133])).
% 0.92/0.70 fof(f3206,plain,(
% 0.92/0.70 ~disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664)),
% 0.92/0.70 inference(cnf_transformation,[status(thm)],[f3204])).
% 0.92/0.70 fof(f5898,plain,(
% 0.92/0.70 ![X0]: (~disjointwith(c_tptpcol_15_93775,X0)|~genls(c_tptpcol_13_18664,X0))),
% 0.92/0.70 inference(resolution,[status(thm)],[f3177,f3206])).
% 0.92/0.70 fof(f6192,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_13_18664,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_15_93775,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f5898,f3180])).
% 0.92/0.70 fof(f6830,plain,(
% 0.92/0.70 ![X0]: (~disjointwith(X0,c_tptpcol_12_18663)|~genls(c_tptpcol_15_93775,X0))),
% 0.92/0.70 inference(resolution,[status(thm)],[f6192,f1438])).
% 0.92/0.70 fof(f6834,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_15_93775,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_12_18663,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f6830,f3177])).
% 0.92/0.70 fof(f6898,plain,(
% 0.92/0.70 ![X0]: (~disjointwith(c_tptpcol_14_93774,X0)|~genls(c_tptpcol_12_18663,X0))),
% 0.92/0.70 inference(resolution,[status(thm)],[f6834,f1399])).
% 0.92/0.70 fof(f6902,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_12_18663,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_14_93774,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f6898,f3180])).
% 0.92/0.70 fof(f6920,plain,(
% 0.92/0.70 ![X0]: (~genls(c_tptpcol_12_18663,X0)|~disjointwith(c_tptpcol_13_93766,X0))),
% 0.92/0.70 inference(resolution,[status(thm)],[f6902,f1413])).
% 0.92/0.70 fof(f6923,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_12_18663,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_13_93766,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f6920,f3180])).
% 0.92/0.70 fof(f6944,plain,(
% 0.92/0.70 ![X0]: (~disjointwith(X0,c_tptpcol_11_18631)|~genls(c_tptpcol_13_93766,X0))),
% 0.92/0.70 inference(resolution,[status(thm)],[f6923,f1292])).
% 0.92/0.70 fof(f6949,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_13_93766,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_11_18631,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f6944,f3177])).
% 0.92/0.70 fof(f6972,plain,(
% 0.92/0.70 ![X0]: (~genls(c_tptpcol_13_93766,X0)|~disjointwith(X0,c_tptpcol_10_18567))),
% 0.92/0.70 inference(resolution,[status(thm)],[f6949,f1389])).
% 0.92/0.70 fof(f6976,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_13_93766,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_10_18567,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f6972,f3177])).
% 0.92/0.70 fof(f6996,plain,(
% 0.92/0.70 ![X0]: (~disjointwith(c_tptpcol_12_93765,X0)|~genls(c_tptpcol_10_18567,X0))),
% 0.92/0.70 inference(resolution,[status(thm)],[f6976,f1246])).
% 0.92/0.70 fof(f7000,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_10_18567,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_12_93765,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f6996,f3180])).
% 0.92/0.70 fof(f7018,plain,(
% 0.92/0.70 ![X0]: (~genls(c_tptpcol_10_18567,X0)|~disjointwith(c_tptpcol_11_93764,X0))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7000,f1237])).
% 0.92/0.70 fof(f7021,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_10_18567,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_11_93764,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7018,f3180])).
% 0.92/0.70 fof(f7042,plain,(
% 0.92/0.70 ![X0]: (~genls(c_tptpcol_10_18567,X0)|~disjointwith(c_tptpcol_10_93700,X0))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7021,f1675])).
% 0.92/0.70 fof(f7045,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_10_18567,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_10_93700,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7042,f3180])).
% 0.92/0.70 fof(f7060,plain,(
% 0.92/0.70 ![X0]: (~genls(c_tptpcol_10_18567,X0)|~disjointwith(c_tptpcol_9_93699,X0))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7045,f1685])).
% 0.92/0.70 fof(f7063,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_10_18567,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_9_93699,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7060,f3180])).
% 0.92/0.70 fof(f7078,plain,(
% 0.92/0.70 ![X0]: (~genls(c_tptpcol_10_18567,X0)|~disjointwith(c_tptpcol_8_93698,X0))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7063,f1672])).
% 0.92/0.70 fof(f7081,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_10_18567,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_8_93698,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7078,f3180])).
% 0.92/0.70 fof(f7096,plain,(
% 0.92/0.70 ![X0]: (~genls(c_tptpcol_10_18567,X0)|~disjointwith(c_tptpcol_7_93186,X0))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7081,f1636])).
% 0.92/0.70 fof(f7099,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_10_18567,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_7_93186,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7096,f3180])).
% 0.92/0.70 fof(f7114,plain,(
% 0.92/0.70 ![X0]: (~disjointwith(X0,c_tptpcol_9_18439)|~genls(c_tptpcol_7_93186,X0))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7099,f1197])).
% 0.92/0.70 fof(f7119,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_7_93186,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_9_18439,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7114,f3177])).
% 0.92/0.70 fof(f7142,plain,(
% 0.92/0.70 ![X0]: (~genls(c_tptpcol_7_93186,X0)|~disjointwith(X0,c_tptpcol_8_18438))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7119,f1505])).
% 0.92/0.70 fof(f7146,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_7_93186,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_8_18438,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7142,f3177])).
% 0.92/0.70 fof(f7166,plain,(
% 0.92/0.70 ![X0]: (~genls(c_tptpcol_7_93186,X0)|~disjointwith(X0,c_tptpcol_7_18437))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7146,f1647])).
% 0.92/0.70 fof(f7170,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_7_93186,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_7_18437,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7166,f3177])).
% 0.92/0.70 fof(f7184,plain,(
% 0.92/0.70 ![X0]: (~genls(c_tptpcol_7_93186,X0)|~disjointwith(X0,c_tptpcol_6_18436))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7170,f1840])).
% 0.92/0.70 fof(f7188,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_7_93186,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_6_18436,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7184,f3177])).
% 0.92/0.70 fof(f7202,plain,(
% 0.92/0.70 ![X0]: (~genls(c_tptpcol_7_93186,X0)|~disjointwith(X0,c_tptpcol_5_16388))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7188,f1644])).
% 0.92/0.70 fof(f7206,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_7_93186,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_5_16388,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7202,f3177])).
% 0.92/0.70 fof(f7220,plain,(
% 0.92/0.70 ![X0]: (~genls(c_tptpcol_7_93186,X0)|~disjointwith(X0,c_tptpcol_4_16387))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7206,f1167])).
% 0.92/0.70 fof(f7224,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_7_93186,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_4_16387,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7220,f3177])).
% 0.92/0.70 fof(f7238,plain,(
% 0.92/0.70 ![X0]: (~disjointwith(c_tptpcol_6_92162,X0)|~genls(c_tptpcol_4_16387,X0))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7224,f1154])).
% 0.92/0.70 fof(f7242,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_6_92162,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7238,f3180])).
% 0.92/0.70 fof(f7260,plain,(
% 0.92/0.70 ![X0]: (~disjointwith(X0,c_tptpcol_3_16386)|~genls(c_tptpcol_6_92162,X0))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7242,f1548])).
% 0.92/0.70 fof(f7265,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_6_92162,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_3_16386,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7260,f3177])).
% 0.92/0.70 fof(f7294,plain,(
% 0.92/0.70 ![X0]: (~genls(c_tptpcol_6_92162,X0)|~disjointwith(X0,c_tptpcol_2_2))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7265,f1694])).
% 0.92/0.70 fof(f7298,plain,(
% 0.92/0.70 ![X0,X1]: (~genls(c_tptpcol_6_92162,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_2_2,X1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7294,f3177])).
% 0.92/0.70 fof(f7318,plain,(
% 0.92/0.70 ![X0]: (~genls(c_tptpcol_6_92162,X0)|~disjointwith(X0,c_tptpcol_1_1))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7298,f1343])).
% 0.92/0.70 fof(f7323,plain,(
% 0.92/0.70 ![X0]: (~genls(c_tptpcol_6_92162,X0)|~disjointwith(c_tptpcol_1_1,X0))),
% 0.92/0.70 inference(resolution,[status(thm)],[f7318,f3174])).
% 0.92/0.72 fof(f7324,plain,(
% 0.92/0.72 ~disjointwith(c_tptpcol_1_1,c_tptpcol_5_90114)),
% 0.92/0.72 inference(resolution,[status(thm)],[f7323,f1741])).
% 0.92/0.72 fof(f7329,plain,(
% 0.92/0.72 ![X0]: (~disjointwith(c_tptpcol_1_1,X0)|~genls(c_tptpcol_5_90114,X0))),
% 0.92/0.72 inference(resolution,[status(thm)],[f7324,f3177])).
% 0.92/0.72 fof(f7342,plain,(
% 0.92/0.72 ~disjointwith(c_tptpcol_1_1,c_tptpcol_4_90113)),
% 0.92/0.72 inference(resolution,[status(thm)],[f7329,f1829])).
% 0.92/0.72 fof(f7346,plain,(
% 0.92/0.72 ![X0]: (~disjointwith(c_tptpcol_1_1,X0)|~genls(c_tptpcol_4_90113,X0))),
% 0.92/0.72 inference(resolution,[status(thm)],[f7342,f3177])).
% 0.92/0.72 fof(f7362,plain,(
% 0.92/0.72 ~disjointwith(c_tptpcol_1_1,c_tptpcol_3_81921)),
% 0.92/0.72 inference(resolution,[status(thm)],[f7346,f1681])).
% 0.92/0.72 fof(f7366,plain,(
% 0.92/0.72 ![X0]: (~disjointwith(c_tptpcol_1_1,X0)|~genls(c_tptpcol_3_81921,X0))),
% 0.92/0.72 inference(resolution,[status(thm)],[f7362,f3177])).
% 0.92/0.72 fof(f7378,plain,(
% 0.92/0.72 ~disjointwith(c_tptpcol_1_1,c_tptpcol_2_65537)),
% 0.92/0.72 inference(resolution,[status(thm)],[f7366,f1194])).
% 0.92/0.72 fof(f7382,plain,(
% 0.92/0.72 ![X0]: (~disjointwith(c_tptpcol_1_1,X0)|~genls(c_tptpcol_2_65537,X0))),
% 0.92/0.72 inference(resolution,[status(thm)],[f7378,f3177])).
% 0.92/0.72 fof(f7394,plain,(
% 0.92/0.72 ~disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)),
% 0.92/0.72 inference(resolution,[status(thm)],[f7382,f1640])).
% 0.92/0.72 fof(f7397,plain,(
% 0.92/0.72 $false),
% 0.92/0.72 inference(forward_subsumption_resolution,[status(thm)],[f7394,f1353])).
% 0.92/0.72 % SZS output end CNFRefutation for theBenchmark.p
% 1.98/1.94 % Elapsed time: 1.385217 seconds
% 1.98/1.94 % CPU time: 2.441278 seconds
% 1.98/1.94 % Total memory used: 151.669 MB
% 1.98/1.94 % Net memory used: 149.570 MB
%------------------------------------------------------------------------------