%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR036+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 : n013.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:41 PM UTC 2026
% Result : Theorem 4.60s 1.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR036+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.09/0.36 % Computer : n013.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.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 14:27:20 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.40 % Drodi V4.1.1
% 4.60/1.06 % Refutation found
% 4.60/1.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.60/1.06 % SZS output start CNFRefutation for theBenchmark
% 4.60/1.06 fof(f6,axiom,(
% 4.60/1.06 genls(c_tptpcol_10_72710,c_tptpcol_9_72709) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f21,axiom,(
% 4.60/1.06 genls(c_tptpcol_9_22021,c_tptpcol_8_22020) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f26,axiom,(
% 4.60/1.06 genls(c_tptpcol_14_72792,c_tptpcol_13_72791) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f28,axiom,(
% 4.60/1.06 genls(c_tptpcol_5_20483,c_tptpcol_4_16387) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f30,axiom,(
% 4.60/1.06 genls(c_tptpcol_11_22023,c_tptpcol_10_22022) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f74,axiom,(
% 4.60/1.06 genls(c_tptpcol_8_72708,c_tptpcol_7_72707) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f145,axiom,(
% 4.60/1.06 genls(c_tptpcol_2_2,c_tptpcol_1_1) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f152,axiom,(
% 4.60/1.06 disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f168,axiom,(
% 4.60/1.06 genls(c_tptpcol_12_22055,c_tptpcol_11_22023) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f189,axiom,(
% 4.60/1.06 genls(c_tptpcol_14_22072,c_tptpcol_13_22071) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f193,axiom,(
% 4.60/1.06 genls(c_tptpcol_10_22022,c_tptpcol_9_22021) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f199,axiom,(
% 4.60/1.06 genls(c_tptpcol_9_72709,c_tptpcol_8_72708) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f224,axiom,(
% 4.60/1.06 genls(c_tptpcol_5_69635,c_tptpcol_4_65539) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f230,axiom,(
% 4.60/1.06 genls(c_tptpcol_13_22071,c_tptpcol_12_22055) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f280,axiom,(
% 4.60/1.06 genls(c_tptpcol_15_72793,c_tptpcol_14_72792) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f285,axiom,(
% 4.60/1.06 genls(c_tptpcol_4_16387,c_tptpcol_3_16386) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f305,axiom,(
% 4.60/1.06 genls(c_tptpcol_8_22020,c_tptpcol_7_21508) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f311,axiom,(
% 4.60/1.06 genls(c_tptpcol_3_65538,c_tptpcol_2_65537) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f335,axiom,(
% 4.60/1.06 genls(c_tptpcol_6_20484,c_tptpcol_5_20483) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f348,axiom,(
% 4.60/1.06 genls(c_tptpcol_2_65537,c_tptpcol_1_65536) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f385,axiom,(
% 4.60/1.06 genls(c_tptpcol_3_16386,c_tptpcol_2_2) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f395,axiom,(
% 4.60/1.06 genls(c_tptpcol_12_72775,c_tptpcol_11_72774) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f397,axiom,(
% 4.60/1.06 genls(c_tptpcol_7_72707,c_tptpcol_6_71683) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f403,axiom,(
% 4.60/1.06 genls(c_tptpcol_16_72795,c_tptpcol_15_72793) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f405,axiom,(
% 4.60/1.06 genls(c_tptpcol_6_71683,c_tptpcol_5_69635) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f436,axiom,(
% 4.60/1.06 genls(c_tptpcol_4_65539,c_tptpcol_3_65538) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f442,axiom,(
% 4.60/1.06 genls(c_tptpcol_15_22076,c_tptpcol_14_22072) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f449,axiom,(
% 4.60/1.06 genls(c_tptpcol_11_72774,c_tptpcol_10_72710) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f456,axiom,(
% 4.60/1.06 genls(c_tptpcol_7_21508,c_tptpcol_6_20484) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f491,axiom,(
% 4.60/1.06 genls(c_tptpcol_13_72791,c_tptpcol_12_72775) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f1121,axiom,(
% 4.60/1.06 (! [ARG1,OLD,NEW] :( ( disjointwith(ARG1,OLD)& genls(NEW,OLD) )=> disjointwith(ARG1,NEW) ) )),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f1122,axiom,(
% 4.60/1.06 (! [OLD,ARG2,NEW] :( ( disjointwith(OLD,ARG2)& genls(NEW,OLD) )=> disjointwith(NEW,ARG2) ) )),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f1132,conjecture,(
% 4.60/1.06 ( mtvisible(c_tptp_member974_mt)=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ) ),
% 4.60/1.06 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.60/1.06 fof(f1133,negated_conjecture,(
% 4.60/1.06 ~(( mtvisible(c_tptp_member974_mt)=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ) )),
% 4.60/1.06 inference(negated_conjecture,[status(cth)],[f1132])).
% 4.60/1.06 fof(f1141,plain,(
% 4.60/1.06 genls(c_tptpcol_10_72710,c_tptpcol_9_72709)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f6])).
% 4.60/1.06 fof(f1164,plain,(
% 4.60/1.06 genls(c_tptpcol_9_22021,c_tptpcol_8_22020)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f21])).
% 4.60/1.06 fof(f1172,plain,(
% 4.60/1.06 genls(c_tptpcol_14_72792,c_tptpcol_13_72791)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f26])).
% 4.60/1.06 fof(f1175,plain,(
% 4.60/1.06 genls(c_tptpcol_5_20483,c_tptpcol_4_16387)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f28])).
% 4.60/1.06 fof(f1178,plain,(
% 4.60/1.06 genls(c_tptpcol_11_22023,c_tptpcol_10_22022)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f30])).
% 4.60/1.06 fof(f1240,plain,(
% 4.60/1.06 genls(c_tptpcol_8_72708,c_tptpcol_7_72707)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f74])).
% 4.60/1.06 fof(f1343,plain,(
% 4.60/1.06 genls(c_tptpcol_2_2,c_tptpcol_1_1)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f145])).
% 4.60/1.06 fof(f1353,plain,(
% 4.60/1.06 disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f152])).
% 4.60/1.06 fof(f1379,plain,(
% 4.60/1.06 genls(c_tptpcol_12_22055,c_tptpcol_11_22023)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f168])).
% 4.60/1.06 fof(f1410,plain,(
% 4.60/1.06 genls(c_tptpcol_14_22072,c_tptpcol_13_22071)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f189])).
% 4.60/1.06 fof(f1416,plain,(
% 4.60/1.06 genls(c_tptpcol_10_22022,c_tptpcol_9_22021)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f193])).
% 4.60/1.06 fof(f1424,plain,(
% 4.60/1.06 genls(c_tptpcol_9_72709,c_tptpcol_8_72708)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f199])).
% 4.60/1.06 fof(f1461,plain,(
% 4.60/1.06 genls(c_tptpcol_5_69635,c_tptpcol_4_65539)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f224])).
% 4.60/1.06 fof(f1470,plain,(
% 4.60/1.06 genls(c_tptpcol_13_22071,c_tptpcol_12_22055)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f230])).
% 4.60/1.06 fof(f1540,plain,(
% 4.60/1.06 genls(c_tptpcol_15_72793,c_tptpcol_14_72792)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f280])).
% 4.60/1.06 fof(f1548,plain,(
% 4.60/1.06 genls(c_tptpcol_4_16387,c_tptpcol_3_16386)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f285])).
% 4.60/1.06 fof(f1581,plain,(
% 4.60/1.06 genls(c_tptpcol_8_22020,c_tptpcol_7_21508)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f305])).
% 4.60/1.06 fof(f1590,plain,(
% 4.60/1.06 genls(c_tptpcol_3_65538,c_tptpcol_2_65537)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f311])).
% 4.60/1.06 fof(f1622,plain,(
% 4.60/1.06 genls(c_tptpcol_6_20484,c_tptpcol_5_20483)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f335])).
% 4.60/1.06 fof(f1640,plain,(
% 4.60/1.06 genls(c_tptpcol_2_65537,c_tptpcol_1_65536)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f348])).
% 4.60/1.06 fof(f1694,plain,(
% 4.60/1.06 genls(c_tptpcol_3_16386,c_tptpcol_2_2)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f385])).
% 4.60/1.06 fof(f1709,plain,(
% 4.60/1.06 genls(c_tptpcol_12_72775,c_tptpcol_11_72774)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f395])).
% 4.60/1.06 fof(f1712,plain,(
% 4.60/1.06 genls(c_tptpcol_7_72707,c_tptpcol_6_71683)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f397])).
% 4.60/1.06 fof(f1721,plain,(
% 4.60/1.06 genls(c_tptpcol_16_72795,c_tptpcol_15_72793)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f403])).
% 4.60/1.06 fof(f1724,plain,(
% 4.60/1.06 genls(c_tptpcol_6_71683,c_tptpcol_5_69635)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f405])).
% 4.60/1.06 fof(f1769,plain,(
% 4.60/1.06 genls(c_tptpcol_4_65539,c_tptpcol_3_65538)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f436])).
% 4.60/1.06 fof(f1779,plain,(
% 4.60/1.06 genls(c_tptpcol_15_22076,c_tptpcol_14_22072)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f442])).
% 4.60/1.06 fof(f1788,plain,(
% 4.60/1.06 genls(c_tptpcol_11_72774,c_tptpcol_10_72710)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f449])).
% 4.60/1.06 fof(f1798,plain,(
% 4.60/1.06 genls(c_tptpcol_7_21508,c_tptpcol_6_20484)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f456])).
% 4.60/1.06 fof(f1852,plain,(
% 4.60/1.06 genls(c_tptpcol_13_72791,c_tptpcol_12_72775)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f491])).
% 4.60/1.06 fof(f3175,plain,(
% 4.60/1.06 ![ARG1,OLD,NEW]: ((~disjointwith(ARG1,OLD)|~genls(NEW,OLD))|disjointwith(ARG1,NEW))),
% 4.60/1.06 inference(pre_NNF_transformation,[status(thm)],[f1121])).
% 4.60/1.06 fof(f3176,plain,(
% 4.60/1.06 ![ARG1,NEW]: ((![OLD]: (~disjointwith(ARG1,OLD)|~genls(NEW,OLD)))|disjointwith(ARG1,NEW))),
% 4.60/1.06 inference(miniscoping,[status(thm)],[f3175])).
% 4.60/1.06 fof(f3177,plain,(
% 4.60/1.06 ![X0,X1,X2]: (~disjointwith(X0,X1)|~genls(X2,X1)|disjointwith(X0,X2))),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f3176])).
% 4.60/1.06 fof(f3178,plain,(
% 4.60/1.06 ![OLD,ARG2,NEW]: ((~disjointwith(OLD,ARG2)|~genls(NEW,OLD))|disjointwith(NEW,ARG2))),
% 4.60/1.06 inference(pre_NNF_transformation,[status(thm)],[f1122])).
% 4.60/1.06 fof(f3179,plain,(
% 4.60/1.06 ![ARG2,NEW]: ((![OLD]: (~disjointwith(OLD,ARG2)|~genls(NEW,OLD)))|disjointwith(NEW,ARG2))),
% 4.60/1.06 inference(miniscoping,[status(thm)],[f3178])).
% 4.60/1.06 fof(f3180,plain,(
% 4.60/1.06 ![X0,X1,X2]: (~disjointwith(X0,X1)|~genls(X2,X0)|disjointwith(X2,X1))),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f3179])).
% 4.60/1.06 fof(f3204,plain,(
% 4.60/1.06 (mtvisible(c_tptp_member974_mt)&~disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795))),
% 4.60/1.06 inference(pre_NNF_transformation,[status(thm)],[f1133])).
% 4.60/1.06 fof(f3206,plain,(
% 4.60/1.06 ~disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)),
% 4.60/1.06 inference(cnf_transformation,[status(thm)],[f3204])).
% 4.60/1.06 fof(f5898,plain,(
% 4.60/1.06 ![X0]: (~disjointwith(c_tptpcol_15_22076,X0)|~genls(c_tptpcol_16_72795,X0))),
% 4.60/1.06 inference(resolution,[status(thm)],[f3177,f3206])).
% 4.60/1.06 fof(f6424,plain,(
% 4.60/1.06 ![X0,X1]: (~genls(c_tptpcol_16_72795,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_15_22076,X1))),
% 4.60/1.06 inference(resolution,[status(thm)],[f5898,f3180])).
% 4.60/1.06 fof(f7354,plain,(
% 4.60/1.06 ![X0]: (~genls(c_tptpcol_16_72795,X0)|~disjointwith(c_tptpcol_14_22072,X0))),
% 4.60/1.06 inference(resolution,[status(thm)],[f6424,f1779])).
% 4.60/1.06 fof(f7357,plain,(
% 4.60/1.06 ![X0,X1]: (~genls(c_tptpcol_16_72795,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_14_22072,X1))),
% 4.60/1.06 inference(resolution,[status(thm)],[f7354,f3180])).
% 4.60/1.06 fof(f7505,plain,(
% 4.60/1.06 ![X0]: (~disjointwith(X0,c_tptpcol_15_72793)|~genls(c_tptpcol_14_22072,X0))),
% 4.60/1.06 inference(resolution,[status(thm)],[f7357,f1721])).
% 4.60/1.06 fof(f7510,plain,(
% 4.60/1.06 ![X0,X1]: (~genls(c_tptpcol_14_22072,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_15_72793,X1))),
% 4.60/1.06 inference(resolution,[status(thm)],[f7505,f3177])).
% 4.60/1.06 fof(f7533,plain,(
% 4.60/1.06 ![X0]: (~genls(c_tptpcol_14_22072,X0)|~disjointwith(X0,c_tptpcol_14_72792))),
% 4.60/1.06 inference(resolution,[status(thm)],[f7510,f1540])).
% 4.60/1.06 fof(f7537,plain,(
% 4.60/1.06 ![X0,X1]: (~genls(c_tptpcol_14_22072,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_14_72792,X1))),
% 4.60/1.06 inference(resolution,[status(thm)],[f7533,f3177])).
% 4.60/1.06 fof(f7557,plain,(
% 4.60/1.06 ![X0]: (~disjointwith(c_tptpcol_13_22071,X0)|~genls(c_tptpcol_14_72792,X0))),
% 4.60/1.06 inference(resolution,[status(thm)],[f7537,f1410])).
% 4.60/1.06 fof(f7561,plain,(
% 4.60/1.06 ![X0,X1]: (~genls(c_tptpcol_14_72792,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_13_22071,X1))),
% 4.60/1.06 inference(resolution,[status(thm)],[f7557,f3180])).
% 4.60/1.06 fof(f7579,plain,(
% 4.60/1.06 ![X0]: (~genls(c_tptpcol_14_72792,X0)|~disjointwith(c_tptpcol_12_22055,X0))),
% 4.60/1.06 inference(resolution,[status(thm)],[f7561,f1470])).
% 4.60/1.06 fof(f7582,plain,(
% 4.60/1.06 ![X0,X1]: (~genls(c_tptpcol_14_72792,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_12_22055,X1))),
% 4.60/1.06 inference(resolution,[status(thm)],[f7579,f3180])).
% 4.60/1.06 fof(f7603,plain,(
% 4.60/1.06 ![X0]: (~genls(c_tptpcol_14_72792,X0)|~disjointwith(c_tptpcol_11_22023,X0))),
% 4.60/1.06 inference(resolution,[status(thm)],[f7582,f1379])).
% 4.60/1.06 fof(f7606,plain,(
% 4.60/1.06 ![X0,X1]: (~genls(c_tptpcol_14_72792,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_11_22023,X1))),
% 4.60/1.06 inference(resolution,[status(thm)],[f7603,f3180])).
% 4.60/1.06 fof(f7621,plain,(
% 4.60/1.06 ![X0]: (~genls(c_tptpcol_14_72792,X0)|~disjointwith(c_tptpcol_10_22022,X0))),
% 4.60/1.06 inference(resolution,[status(thm)],[f7606,f1178])).
% 4.60/1.06 fof(f7624,plain,(
% 4.60/1.06 ![X0,X1]: (~genls(c_tptpcol_14_72792,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_10_22022,X1))),
% 4.60/1.06 inference(resolution,[status(thm)],[f7621,f3180])).
% 4.60/1.06 fof(f7639,plain,(
% 4.60/1.06 ![X0]: (~genls(c_tptpcol_14_72792,X0)|~disjointwith(c_tptpcol_9_22021,X0))),
% 4.60/1.06 inference(resolution,[status(thm)],[f7624,f1416])).
% 4.60/1.06 fof(f7642,plain,(
% 4.60/1.06 ![X0,X1]: (~genls(c_tptpcol_14_72792,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_9_22021,X1))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7639,f3180])).
% 4.60/1.07 fof(f7657,plain,(
% 4.60/1.07 ![X0]: (~disjointwith(X0,c_tptpcol_13_72791)|~genls(c_tptpcol_9_22021,X0))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7642,f1172])).
% 4.60/1.07 fof(f7662,plain,(
% 4.60/1.07 ![X0,X1]: (~genls(c_tptpcol_9_22021,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_13_72791,X1))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7657,f3177])).
% 4.60/1.07 fof(f7685,plain,(
% 4.60/1.07 ![X0]: (~genls(c_tptpcol_9_22021,X0)|~disjointwith(X0,c_tptpcol_12_72775))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7662,f1852])).
% 4.60/1.07 fof(f7689,plain,(
% 4.60/1.07 ![X0,X1]: (~genls(c_tptpcol_9_22021,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_12_72775,X1))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7685,f3177])).
% 4.60/1.07 fof(f7709,plain,(
% 4.60/1.07 ![X0]: (~genls(c_tptpcol_9_22021,X0)|~disjointwith(X0,c_tptpcol_11_72774))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7689,f1709])).
% 4.60/1.07 fof(f7713,plain,(
% 4.60/1.07 ![X0,X1]: (~genls(c_tptpcol_9_22021,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_11_72774,X1))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7709,f3177])).
% 4.60/1.07 fof(f7727,plain,(
% 4.60/1.07 ![X0]: (~genls(c_tptpcol_9_22021,X0)|~disjointwith(X0,c_tptpcol_10_72710))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7713,f1788])).
% 4.60/1.07 fof(f7731,plain,(
% 4.60/1.07 ![X0,X1]: (~genls(c_tptpcol_9_22021,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_10_72710,X1))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7727,f3177])).
% 4.60/1.07 fof(f7745,plain,(
% 4.60/1.07 ![X0]: (~disjointwith(c_tptpcol_8_22020,X0)|~genls(c_tptpcol_10_72710,X0))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7731,f1164])).
% 4.60/1.07 fof(f7749,plain,(
% 4.60/1.07 ![X0,X1]: (~genls(c_tptpcol_10_72710,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_8_22020,X1))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7745,f3180])).
% 4.60/1.07 fof(f7767,plain,(
% 4.60/1.07 ![X0]: (~genls(c_tptpcol_10_72710,X0)|~disjointwith(c_tptpcol_7_21508,X0))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7749,f1581])).
% 4.60/1.07 fof(f7770,plain,(
% 4.60/1.07 ![X0,X1]: (~genls(c_tptpcol_10_72710,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_7_21508,X1))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7767,f3180])).
% 4.60/1.07 fof(f7791,plain,(
% 4.60/1.07 ![X0]: (~genls(c_tptpcol_10_72710,X0)|~disjointwith(c_tptpcol_6_20484,X0))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7770,f1798])).
% 4.60/1.07 fof(f7794,plain,(
% 4.60/1.07 ![X0,X1]: (~genls(c_tptpcol_10_72710,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_6_20484,X1))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7791,f3180])).
% 4.60/1.07 fof(f7809,plain,(
% 4.60/1.07 ![X0]: (~genls(c_tptpcol_10_72710,X0)|~disjointwith(c_tptpcol_5_20483,X0))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7794,f1622])).
% 4.60/1.07 fof(f7812,plain,(
% 4.60/1.07 ![X0,X1]: (~genls(c_tptpcol_10_72710,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_5_20483,X1))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7809,f3180])).
% 4.60/1.07 fof(f7827,plain,(
% 4.60/1.07 ![X0]: (~genls(c_tptpcol_10_72710,X0)|~disjointwith(c_tptpcol_4_16387,X0))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7812,f1175])).
% 4.60/1.07 fof(f7830,plain,(
% 4.60/1.07 ![X0,X1]: (~genls(c_tptpcol_10_72710,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_4_16387,X1))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7827,f3180])).
% 4.60/1.07 fof(f7845,plain,(
% 4.60/1.07 ![X0]: (~disjointwith(X0,c_tptpcol_9_72709)|~genls(c_tptpcol_4_16387,X0))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7830,f1141])).
% 4.60/1.07 fof(f7850,plain,(
% 4.60/1.07 ![X0,X1]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_9_72709,X1))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7845,f3177])).
% 4.60/1.07 fof(f7873,plain,(
% 4.60/1.07 ![X0]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,c_tptpcol_8_72708))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7850,f1424])).
% 4.60/1.07 fof(f7877,plain,(
% 4.60/1.07 ![X0,X1]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_8_72708,X1))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7873,f3177])).
% 4.60/1.07 fof(f7897,plain,(
% 4.60/1.07 ![X0]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,c_tptpcol_7_72707))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7877,f1240])).
% 4.60/1.07 fof(f7901,plain,(
% 4.60/1.07 ![X0,X1]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_7_72707,X1))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7897,f3177])).
% 4.60/1.07 fof(f7915,plain,(
% 4.60/1.07 ![X0]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,c_tptpcol_6_71683))),
% 4.60/1.07 inference(resolution,[status(thm)],[f7901,f1712])).
% 4.60/1.07 fof(f7919,plain,(
% 4.60/1.09 ![X0,X1]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_6_71683,X1))),
% 4.60/1.09 inference(resolution,[status(thm)],[f7915,f3177])).
% 4.60/1.09 fof(f7933,plain,(
% 4.60/1.09 ![X0]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,c_tptpcol_5_69635))),
% 4.60/1.09 inference(resolution,[status(thm)],[f7919,f1724])).
% 4.60/1.09 fof(f7937,plain,(
% 4.60/1.09 ![X0,X1]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_5_69635,X1))),
% 4.60/1.09 inference(resolution,[status(thm)],[f7933,f3177])).
% 4.60/1.09 fof(f7951,plain,(
% 4.60/1.09 ![X0]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,c_tptpcol_4_65539))),
% 4.60/1.09 inference(resolution,[status(thm)],[f7937,f1461])).
% 4.60/1.09 fof(f7955,plain,(
% 4.60/1.09 ![X0,X1]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_4_65539,X1))),
% 4.60/1.09 inference(resolution,[status(thm)],[f7951,f3177])).
% 4.60/1.09 fof(f7969,plain,(
% 4.60/1.09 ![X0]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,c_tptpcol_3_65538))),
% 4.60/1.09 inference(resolution,[status(thm)],[f7955,f1769])).
% 4.60/1.09 fof(f7973,plain,(
% 4.60/1.09 ![X0,X1]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_3_65538,X1))),
% 4.60/1.10 inference(resolution,[status(thm)],[f7969,f3177])).
% 4.60/1.10 fof(f7987,plain,(
% 4.60/1.10 ![X0]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,c_tptpcol_2_65537))),
% 4.60/1.10 inference(resolution,[status(thm)],[f7973,f1590])).
% 4.60/1.10 fof(f7991,plain,(
% 4.60/1.10 ![X0,X1]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_2_65537,X1))),
% 4.60/1.10 inference(resolution,[status(thm)],[f7987,f3177])).
% 4.60/1.10 fof(f8005,plain,(
% 4.60/1.10 ![X0]: (~genls(c_tptpcol_4_16387,X0)|~disjointwith(X0,c_tptpcol_1_65536))),
% 4.60/1.10 inference(resolution,[status(thm)],[f7991,f1640])).
% 4.60/1.10 fof(f8008,plain,(
% 4.60/1.10 ~disjointwith(c_tptpcol_3_16386,c_tptpcol_1_65536)),
% 4.60/1.10 inference(resolution,[status(thm)],[f8005,f1548])).
% 4.60/1.10 fof(f8012,plain,(
% 4.60/1.10 ![X0]: (~disjointwith(X0,c_tptpcol_1_65536)|~genls(c_tptpcol_3_16386,X0))),
% 4.60/1.10 inference(resolution,[status(thm)],[f8008,f3180])).
% 4.60/1.10 fof(f8024,plain,(
% 4.60/1.10 ~disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536)),
% 4.60/1.10 inference(resolution,[status(thm)],[f8012,f1694])).
% 4.60/1.10 fof(f8027,plain,(
% 4.60/1.10 ![X0]: (~disjointwith(X0,c_tptpcol_1_65536)|~genls(c_tptpcol_2_2,X0))),
% 4.60/1.10 inference(resolution,[status(thm)],[f8024,f3180])).
% 4.60/1.10 fof(f8051,plain,(
% 4.60/1.10 ~disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)),
% 4.60/1.10 inference(resolution,[status(thm)],[f8027,f1343])).
% 4.60/1.10 fof(f8054,plain,(
% 4.60/1.10 $false),
% 4.60/1.10 inference(forward_subsumption_resolution,[status(thm)],[f8051,f1353])).
% 4.60/1.10 % SZS output end CNFRefutation for theBenchmark.p
% 2.47/2.29 % Elapsed time: 1.705236 seconds
% 2.47/2.29 % CPU time: 5.074607 seconds
% 2.47/2.29 % Total memory used: 203.047 MB
% 2.47/2.29 % Net memory used: 197.969 MB
%------------------------------------------------------------------------------