%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR049+2 : 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 : 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:48 PM UTC 2026
% Result : Theorem 5.94s 16.33s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR049+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/15.40 % Computer : n010.cluster.edu
% 0.12/15.40 % Model : x86_64 x86_64
% 0.12/15.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/15.40 % Memory : 8046.5625MB
% 0.12/15.40 % OS : Linux 6.8.0-71-generic
% 0.12/15.40 % CPULimit : 300
% 0.12/15.40 % WCLimit : 300
% 0.12/15.40 % DateTime : Mon Sep 21 14:35:55 UTC 2026
% 0.12/15.40 % CPUTime :
% 0.12/15.45 % Drodi V4.1.1
% 5.94/16.33 % Refutation found
% 5.94/16.33 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.94/16.33 % SZS output start CNFRefutation for theBenchmark
% 5.94/16.33 fof(f41,axiom,(
% 5.94/16.33 genls(c_tptpcol_3_81921,c_tptpcol_2_65537) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f47,axiom,(
% 5.94/16.33 genls(c_tptpcol_11_92230,c_tptpcol_10_92166) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f89,axiom,(
% 5.94/16.33 genls(c_tptpcol_12_92262,c_tptpcol_11_92230) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f102,axiom,(
% 5.94/16.33 genls(c_tptpcol_15_92268,c_tptpcol_14_92264) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f118,axiom,(
% 5.94/16.33 genls(c_tptpcol_5_24579,c_tptpcol_4_24578) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f141,axiom,(
% 5.94/16.33 genls(c_tptpcol_12_26919,c_tptpcol_11_26887) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f145,axiom,(
% 5.94/16.33 genls(c_tptpcol_2_2,c_tptpcol_1_1) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f148,axiom,(
% 5.94/16.33 genls(c_tptpcol_9_92165,c_tptpcol_8_92164) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f152,axiom,(
% 5.94/16.33 disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f222,axiom,(
% 5.94/16.33 genls(c_tptpcol_4_24578,c_tptpcol_3_16386) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f239,axiom,(
% 5.94/16.33 genls(c_tptpcol_8_26629,c_tptpcol_7_26628) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f261,axiom,(
% 5.94/16.33 genls(c_tptpcol_7_26628,c_tptpcol_6_26627) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f267,axiom,(
% 5.94/16.33 genls(c_tptpcol_16_92269,c_tptpcol_15_92268) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f277,axiom,(
% 5.94/16.33 genls(c_tptpcol_10_26886,c_tptpcol_9_26885) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f313,axiom,(
% 5.94/16.33 genls(c_tptpcol_14_26921,c_tptpcol_13_26920) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f324,axiom,(
% 5.94/16.33 genls(c_tptpcol_7_92163,c_tptpcol_6_92162) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f348,axiom,(
% 5.94/16.33 genls(c_tptpcol_2_65537,c_tptpcol_1_65536) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f374,axiom,(
% 5.94/16.33 genls(c_tptpcol_6_26627,c_tptpcol_5_24579) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f376,axiom,(
% 5.94/16.33 genls(c_tptpcol_4_90113,c_tptpcol_3_81921) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f385,axiom,(
% 5.94/16.33 genls(c_tptpcol_3_16386,c_tptpcol_2_2) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f410,axiom,(
% 5.94/16.33 genls(c_tptpcol_9_26885,c_tptpcol_8_26629) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f417,axiom,(
% 5.94/16.33 genls(c_tptpcol_6_92162,c_tptpcol_5_90114) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f420,axiom,(
% 5.94/16.33 genls(c_tptpcol_8_92164,c_tptpcol_7_92163) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f429,axiom,(
% 5.94/16.33 genls(c_tptpcol_11_26887,c_tptpcol_10_26886) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f431,axiom,(
% 5.94/16.33 genls(c_tptpcol_16_26926,c_tptpcol_15_26925) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f465,axiom,(
% 5.94/16.33 genls(c_tptpcol_13_26920,c_tptpcol_12_26919) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f467,axiom,(
% 5.94/16.33 genls(c_tptpcol_14_92264,c_tptpcol_13_92263) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f473,axiom,(
% 5.94/16.33 genls(c_tptpcol_13_92263,c_tptpcol_12_92262) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f476,axiom,(
% 5.94/16.33 genls(c_tptpcol_5_90114,c_tptpcol_4_90113) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f480,axiom,(
% 5.94/16.33 genls(c_tptpcol_15_26925,c_tptpcol_14_26921) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f497,axiom,(
% 5.94/16.33 genls(c_tptpcol_10_92166,c_tptpcol_9_92165) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f1121,axiom,(
% 5.94/16.33 (! [ARG1,OLD,NEW] :( ( disjointwith(ARG1,OLD)& genls(NEW,OLD) )=> disjointwith(ARG1,NEW) ) )),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f1122,axiom,(
% 5.94/16.33 (! [OLD,ARG2,NEW] :( ( disjointwith(OLD,ARG2)& genls(NEW,OLD) )=> disjointwith(NEW,ARG2) ) )),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f1132,conjecture,(
% 5.94/16.33 ( mtvisible(c_unitedstatesgeographypeoplemt)=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ) ),
% 5.94/16.33 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.94/16.33 fof(f1133,negated_conjecture,(
% 5.94/16.33 ~(( mtvisible(c_unitedstatesgeographypeoplemt)=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ) )),
% 5.94/16.33 inference(negated_conjecture,[status(cth)],[f1132])).
% 5.94/16.33 fof(f1194,plain,(
% 5.94/16.33 genls(c_tptpcol_3_81921,c_tptpcol_2_65537)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f41])).
% 5.94/16.33 fof(f1203,plain,(
% 5.94/16.33 genls(c_tptpcol_11_92230,c_tptpcol_10_92166)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f47])).
% 5.94/16.33 fof(f1262,plain,(
% 5.94/16.33 genls(c_tptpcol_12_92262,c_tptpcol_11_92230)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f89])).
% 5.94/16.33 fof(f1280,plain,(
% 5.94/16.33 genls(c_tptpcol_15_92268,c_tptpcol_14_92264)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f102])).
% 5.94/16.33 fof(f1305,plain,(
% 5.94/16.33 genls(c_tptpcol_5_24579,c_tptpcol_4_24578)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f118])).
% 5.94/16.33 fof(f1337,plain,(
% 5.94/16.33 genls(c_tptpcol_12_26919,c_tptpcol_11_26887)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f141])).
% 5.94/16.33 fof(f1343,plain,(
% 5.94/16.33 genls(c_tptpcol_2_2,c_tptpcol_1_1)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f145])).
% 5.94/16.33 fof(f1347,plain,(
% 5.94/16.33 genls(c_tptpcol_9_92165,c_tptpcol_8_92164)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f148])).
% 5.94/16.33 fof(f1353,plain,(
% 5.94/16.33 disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f152])).
% 5.94/16.33 fof(f1458,plain,(
% 5.94/16.33 genls(c_tptpcol_4_24578,c_tptpcol_3_16386)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f222])).
% 5.94/16.33 fof(f1483,plain,(
% 5.94/16.33 genls(c_tptpcol_8_26629,c_tptpcol_7_26628)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f239])).
% 5.94/16.33 fof(f1513,plain,(
% 5.94/16.33 genls(c_tptpcol_7_26628,c_tptpcol_6_26627)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f261])).
% 5.94/16.33 fof(f1523,plain,(
% 5.94/16.33 genls(c_tptpcol_16_92269,c_tptpcol_15_92268)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f267])).
% 5.94/16.33 fof(f1536,plain,(
% 5.94/16.33 genls(c_tptpcol_10_26886,c_tptpcol_9_26885)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f277])).
% 5.94/16.33 fof(f1593,plain,(
% 5.94/16.33 genls(c_tptpcol_14_26921,c_tptpcol_13_26920)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f313])).
% 5.94/16.33 fof(f1608,plain,(
% 5.94/16.33 genls(c_tptpcol_7_92163,c_tptpcol_6_92162)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f324])).
% 5.94/16.33 fof(f1640,plain,(
% 5.94/16.33 genls(c_tptpcol_2_65537,c_tptpcol_1_65536)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f348])).
% 5.94/16.33 fof(f1678,plain,(
% 5.94/16.33 genls(c_tptpcol_6_26627,c_tptpcol_5_24579)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f374])).
% 5.94/16.33 fof(f1681,plain,(
% 5.94/16.33 genls(c_tptpcol_4_90113,c_tptpcol_3_81921)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f376])).
% 5.94/16.33 fof(f1694,plain,(
% 5.94/16.33 genls(c_tptpcol_3_16386,c_tptpcol_2_2)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f385])).
% 5.94/16.33 fof(f1731,plain,(
% 5.94/16.33 genls(c_tptpcol_9_26885,c_tptpcol_8_26629)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f410])).
% 5.94/16.33 fof(f1741,plain,(
% 5.94/16.33 genls(c_tptpcol_6_92162,c_tptpcol_5_90114)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f417])).
% 5.94/16.33 fof(f1745,plain,(
% 5.94/16.33 genls(c_tptpcol_8_92164,c_tptpcol_7_92163)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f420])).
% 5.94/16.33 fof(f1758,plain,(
% 5.94/16.33 genls(c_tptpcol_11_26887,c_tptpcol_10_26886)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f429])).
% 5.94/16.33 fof(f1761,plain,(
% 5.94/16.33 genls(c_tptpcol_16_26926,c_tptpcol_15_26925)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f431])).
% 5.94/16.33 fof(f1813,plain,(
% 5.94/16.33 genls(c_tptpcol_13_26920,c_tptpcol_12_26919)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f465])).
% 5.94/16.33 fof(f1816,plain,(
% 5.94/16.33 genls(c_tptpcol_14_92264,c_tptpcol_13_92263)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f467])).
% 5.94/16.33 fof(f1825,plain,(
% 5.94/16.33 genls(c_tptpcol_13_92263,c_tptpcol_12_92262)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f473])).
% 5.94/16.33 fof(f1829,plain,(
% 5.94/16.33 genls(c_tptpcol_5_90114,c_tptpcol_4_90113)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f476])).
% 5.94/16.33 fof(f1835,plain,(
% 5.94/16.33 genls(c_tptpcol_15_26925,c_tptpcol_14_26921)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f480])).
% 5.94/16.33 fof(f1862,plain,(
% 5.94/16.33 genls(c_tptpcol_10_92166,c_tptpcol_9_92165)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f497])).
% 5.94/16.33 fof(f3175,plain,(
% 5.94/16.33 ![ARG1,OLD,NEW]: ((~disjointwith(ARG1,OLD)|~genls(NEW,OLD))|disjointwith(ARG1,NEW))),
% 5.94/16.33 inference(pre_NNF_transformation,[status(thm)],[f1121])).
% 5.94/16.33 fof(f3176,plain,(
% 5.94/16.33 ![ARG1,NEW]: ((![OLD]: (~disjointwith(ARG1,OLD)|~genls(NEW,OLD)))|disjointwith(ARG1,NEW))),
% 5.94/16.33 inference(miniscoping,[status(thm)],[f3175])).
% 5.94/16.33 fof(f3177,plain,(
% 5.94/16.33 ![X0,X1,X2]: (~disjointwith(X0,X1)|~genls(X2,X1)|disjointwith(X0,X2))),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f3176])).
% 5.94/16.33 fof(f3178,plain,(
% 5.94/16.33 ![OLD,ARG2,NEW]: ((~disjointwith(OLD,ARG2)|~genls(NEW,OLD))|disjointwith(NEW,ARG2))),
% 5.94/16.33 inference(pre_NNF_transformation,[status(thm)],[f1122])).
% 5.94/16.33 fof(f3179,plain,(
% 5.94/16.33 ![ARG2,NEW]: ((![OLD]: (~disjointwith(OLD,ARG2)|~genls(NEW,OLD)))|disjointwith(NEW,ARG2))),
% 5.94/16.33 inference(miniscoping,[status(thm)],[f3178])).
% 5.94/16.33 fof(f3180,plain,(
% 5.94/16.33 ![X0,X1,X2]: (~disjointwith(X0,X1)|~genls(X2,X0)|disjointwith(X2,X1))),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f3179])).
% 5.94/16.33 fof(f3204,plain,(
% 5.94/16.33 (mtvisible(c_unitedstatesgeographypeoplemt)&~disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269))),
% 5.94/16.33 inference(pre_NNF_transformation,[status(thm)],[f1133])).
% 5.94/16.33 fof(f3206,plain,(
% 5.94/16.33 ~disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269)),
% 5.94/16.33 inference(cnf_transformation,[status(thm)],[f3204])).
% 5.94/16.33 fof(f5898,plain,(
% 5.94/16.33 ![X0]: (~disjointwith(c_tptpcol_16_26926,X0)|~genls(c_tptpcol_16_92269,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f3177,f3206])).
% 5.94/16.33 fof(f6207,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_16_92269,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_16_26926,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f5898,f3180])).
% 5.94/16.33 fof(f6857,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_16_92269,X0)|~disjointwith(c_tptpcol_15_26925,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f6207,f1761])).
% 5.94/16.33 fof(f6860,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_16_92269,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_15_26925,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f6857,f3180])).
% 5.94/16.33 fof(f6922,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_16_92269,X0)|~disjointwith(c_tptpcol_14_26921,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f6860,f1835])).
% 5.94/16.33 fof(f6925,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_16_92269,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_14_26921,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f6922,f3180])).
% 5.94/16.33 fof(f6940,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_16_92269,X0)|~disjointwith(c_tptpcol_13_26920,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f6925,f1593])).
% 5.94/16.33 fof(f6943,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_16_92269,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_13_26920,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f6940,f3180])).
% 5.94/16.33 fof(f6958,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_16_92269,X0)|~disjointwith(c_tptpcol_12_26919,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f6943,f1813])).
% 5.94/16.33 fof(f6961,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_16_92269,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_12_26919,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f6958,f3180])).
% 5.94/16.33 fof(f6976,plain,(
% 5.94/16.33 ![X0]: (~disjointwith(X0,c_tptpcol_15_92268)|~genls(c_tptpcol_12_26919,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f6961,f1523])).
% 5.94/16.33 fof(f6981,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_12_26919,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_15_92268,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f6976,f3177])).
% 5.94/16.33 fof(f7004,plain,(
% 5.94/16.33 ![X0]: (~disjointwith(c_tptpcol_11_26887,X0)|~genls(c_tptpcol_15_92268,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f6981,f1337])).
% 5.94/16.33 fof(f7008,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_11_26887,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7004,f3180])).
% 5.94/16.33 fof(f7032,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(c_tptpcol_10_26886,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7008,f1758])).
% 5.94/16.33 fof(f7035,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_10_26886,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7032,f3180])).
% 5.94/16.33 fof(f7056,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(c_tptpcol_9_26885,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7035,f1536])).
% 5.94/16.33 fof(f7059,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_9_26885,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7056,f3180])).
% 5.94/16.33 fof(f7074,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(c_tptpcol_8_26629,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7059,f1731])).
% 5.94/16.33 fof(f7077,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_8_26629,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7074,f3180])).
% 5.94/16.33 fof(f7092,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(c_tptpcol_7_26628,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7077,f1483])).
% 5.94/16.33 fof(f7095,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_7_26628,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7092,f3180])).
% 5.94/16.33 fof(f7110,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(c_tptpcol_6_26627,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7095,f1513])).
% 5.94/16.33 fof(f7113,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_6_26627,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7110,f3180])).
% 5.94/16.33 fof(f7128,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(c_tptpcol_5_24579,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7113,f1678])).
% 5.94/16.33 fof(f7131,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_5_24579,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7128,f3180])).
% 5.94/16.33 fof(f7146,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(c_tptpcol_4_24578,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7131,f1305])).
% 5.94/16.33 fof(f7149,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_4_24578,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7146,f3180])).
% 5.94/16.33 fof(f7164,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(c_tptpcol_3_16386,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7149,f1458])).
% 5.94/16.33 fof(f7167,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_15_92268,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_3_16386,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7164,f3180])).
% 5.94/16.33 fof(f7182,plain,(
% 5.94/16.33 ![X0]: (~disjointwith(X0,c_tptpcol_14_92264)|~genls(c_tptpcol_3_16386,X0))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7167,f1280])).
% 5.94/16.33 fof(f7187,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_14_92264,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7182,f3177])).
% 5.94/16.33 fof(f7210,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,c_tptpcol_13_92263))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7187,f1816])).
% 5.94/16.33 fof(f7214,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_13_92263,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7210,f3177])).
% 5.94/16.33 fof(f7234,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,c_tptpcol_12_92262))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7214,f1825])).
% 5.94/16.33 fof(f7238,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_12_92262,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7234,f3177])).
% 5.94/16.33 fof(f7252,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,c_tptpcol_11_92230))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7238,f1262])).
% 5.94/16.33 fof(f7256,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_11_92230,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7252,f3177])).
% 5.94/16.33 fof(f7270,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,c_tptpcol_10_92166))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7256,f1203])).
% 5.94/16.33 fof(f7274,plain,(
% 5.94/16.33 ![X0,X1]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_10_92166,X1))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7270,f3177])).
% 5.94/16.33 fof(f7288,plain,(
% 5.94/16.33 ![X0]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,c_tptpcol_9_92165))),
% 5.94/16.33 inference(resolution,[status(thm)],[f7274,f1862])).
% 5.94/16.37 fof(f7292,plain,(
% 5.94/16.37 ![X0,X1]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_9_92165,X1))),
% 5.94/16.37 inference(resolution,[status(thm)],[f7288,f3177])).
% 5.94/16.37 fof(f7306,plain,(
% 5.94/16.37 ![X0]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,c_tptpcol_8_92164))),
% 5.94/16.37 inference(resolution,[status(thm)],[f7292,f1347])).
% 5.94/16.37 fof(f7310,plain,(
% 5.94/16.37 ![X0,X1]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_8_92164,X1))),
% 5.94/16.37 inference(resolution,[status(thm)],[f7306,f3177])).
% 5.94/16.37 fof(f7324,plain,(
% 5.94/16.37 ![X0]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,c_tptpcol_7_92163))),
% 5.94/16.37 inference(resolution,[status(thm)],[f7310,f1745])).
% 5.94/16.37 fof(f7328,plain,(
% 5.94/16.37 ![X0,X1]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_7_92163,X1))),
% 5.94/16.37 inference(resolution,[status(thm)],[f7324,f3177])).
% 5.94/16.37 fof(f7342,plain,(
% 5.94/16.37 ![X0]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,c_tptpcol_6_92162))),
% 5.94/16.37 inference(resolution,[status(thm)],[f7328,f1608])).
% 5.94/16.37 fof(f7346,plain,(
% 5.94/16.37 ![X0,X1]: (~genls(c_tptpcol_3_16386,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_6_92162,X1))),
% 5.94/16.37 inference(resolution,[status(thm)],[f7342,f3177])).
% 5.94/16.37 fof(f7360,plain,(
% 5.94/16.37 ![X0]: (~disjointwith(c_tptpcol_2_2,X0)|~genls(c_tptpcol_6_92162,X0))),
% 5.94/16.37 inference(resolution,[status(thm)],[f7346,f1694])).
% 5.94/16.37 fof(f7364,plain,(
% 5.94/16.37 ![X0,X1]: (~genls(c_tptpcol_6_92162,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_2_2,X1))),
% 5.94/16.37 inference(resolution,[status(thm)],[f7360,f3180])).
% 5.94/16.37 fof(f7382,plain,(
% 5.94/16.37 ![X0]: (~genls(c_tptpcol_6_92162,X0)|~disjointwith(c_tptpcol_1_1,X0))),
% 5.94/16.37 inference(resolution,[status(thm)],[f7364,f1343])).
% 5.94/16.37 fof(f7385,plain,(
% 5.94/16.37 ~disjointwith(c_tptpcol_1_1,c_tptpcol_5_90114)),
% 5.94/16.37 inference(resolution,[status(thm)],[f7382,f1741])).
% 5.94/16.37 fof(f7390,plain,(
% 5.94/16.37 ![X0]: (~disjointwith(c_tptpcol_1_1,X0)|~genls(c_tptpcol_5_90114,X0))),
% 5.94/16.37 inference(resolution,[status(thm)],[f7385,f3177])).
% 5.94/16.37 fof(f7403,plain,(
% 5.94/16.37 ~disjointwith(c_tptpcol_1_1,c_tptpcol_4_90113)),
% 5.94/16.37 inference(resolution,[status(thm)],[f7390,f1829])).
% 5.94/16.37 fof(f7407,plain,(
% 5.94/16.37 ![X0]: (~disjointwith(c_tptpcol_1_1,X0)|~genls(c_tptpcol_4_90113,X0))),
% 5.94/16.37 inference(resolution,[status(thm)],[f7403,f3177])).
% 5.94/16.37 fof(f7427,plain,(
% 5.94/16.37 ~disjointwith(c_tptpcol_1_1,c_tptpcol_3_81921)),
% 5.94/16.37 inference(resolution,[status(thm)],[f7407,f1681])).
% 5.94/16.37 fof(f7431,plain,(
% 5.94/16.37 ![X0]: (~disjointwith(c_tptpcol_1_1,X0)|~genls(c_tptpcol_3_81921,X0))),
% 5.94/16.37 inference(resolution,[status(thm)],[f7427,f3177])).
% 5.94/16.37 fof(f7443,plain,(
% 5.94/16.37 ~disjointwith(c_tptpcol_1_1,c_tptpcol_2_65537)),
% 5.94/16.37 inference(resolution,[status(thm)],[f7431,f1194])).
% 5.94/16.37 fof(f7447,plain,(
% 5.94/16.37 ![X0]: (~disjointwith(c_tptpcol_1_1,X0)|~genls(c_tptpcol_2_65537,X0))),
% 5.94/16.37 inference(resolution,[status(thm)],[f7443,f3177])).
% 5.94/16.37 fof(f7459,plain,(
% 5.94/16.37 ~disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)),
% 5.94/16.37 inference(resolution,[status(thm)],[f7447,f1640])).
% 5.94/16.37 fof(f7462,plain,(
% 5.94/16.37 $false),
% 5.94/16.37 inference(forward_subsumption_resolution,[status(thm)],[f7459,f1353])).
% 5.94/16.37 % SZS output end CNFRefutation for theBenchmark.p
% 2.96/17.58 % Elapsed time: 1.956400 seconds
% 2.96/17.58 % CPU time: 6.894748 seconds
% 2.96/17.58 % Total memory used: 198.449 MB
% 2.96/17.58 % Net memory used: 194.529 MB
%------------------------------------------------------------------------------