%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR036+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 0.12s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR036+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n020.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:28:47 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 0.12/0.42 % Refutation found
% 0.12/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.42 fof(f6,axiom,(
% 0.12/0.42 genls(c_tptpcol_2_2,c_tptpcol_1_1) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f8,axiom,(
% 0.12/0.42 genls(c_tptpcol_3_16386,c_tptpcol_2_2) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f10,axiom,(
% 0.12/0.42 genls(c_tptpcol_4_16387,c_tptpcol_3_16386) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f12,axiom,(
% 0.12/0.42 genls(c_tptpcol_5_20483,c_tptpcol_4_16387) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f14,axiom,(
% 0.12/0.42 genls(c_tptpcol_6_20484,c_tptpcol_5_20483) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f16,axiom,(
% 0.12/0.42 genls(c_tptpcol_7_21508,c_tptpcol_6_20484) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f18,axiom,(
% 0.12/0.42 genls(c_tptpcol_8_22020,c_tptpcol_7_21508) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f20,axiom,(
% 0.12/0.42 genls(c_tptpcol_9_22021,c_tptpcol_8_22020) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f22,axiom,(
% 0.12/0.42 genls(c_tptpcol_10_22022,c_tptpcol_9_22021) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f24,axiom,(
% 0.12/0.42 genls(c_tptpcol_11_22023,c_tptpcol_10_22022) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f26,axiom,(
% 0.12/0.42 genls(c_tptpcol_12_22055,c_tptpcol_11_22023) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f28,axiom,(
% 0.12/0.42 genls(c_tptpcol_13_22071,c_tptpcol_12_22055) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f30,axiom,(
% 0.12/0.42 genls(c_tptpcol_14_22072,c_tptpcol_13_22071) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f32,axiom,(
% 0.12/0.42 genls(c_tptpcol_15_22076,c_tptpcol_14_22072) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f34,axiom,(
% 0.12/0.42 genls(c_tptpcol_2_65537,c_tptpcol_1_65536) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f36,axiom,(
% 0.12/0.42 genls(c_tptpcol_3_65538,c_tptpcol_2_65537) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f38,axiom,(
% 0.12/0.42 genls(c_tptpcol_4_65539,c_tptpcol_3_65538) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f40,axiom,(
% 0.12/0.42 genls(c_tptpcol_5_69635,c_tptpcol_4_65539) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f42,axiom,(
% 0.12/0.42 genls(c_tptpcol_6_71683,c_tptpcol_5_69635) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f44,axiom,(
% 0.12/0.42 genls(c_tptpcol_7_72707,c_tptpcol_6_71683) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f46,axiom,(
% 0.12/0.42 genls(c_tptpcol_8_72708,c_tptpcol_7_72707) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f48,axiom,(
% 0.12/0.42 genls(c_tptpcol_9_72709,c_tptpcol_8_72708) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f50,axiom,(
% 0.12/0.42 genls(c_tptpcol_10_72710,c_tptpcol_9_72709) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f52,axiom,(
% 0.12/0.42 genls(c_tptpcol_11_72774,c_tptpcol_10_72710) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f54,axiom,(
% 0.12/0.42 genls(c_tptpcol_12_72775,c_tptpcol_11_72774) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f56,axiom,(
% 0.12/0.42 genls(c_tptpcol_13_72791,c_tptpcol_12_72775) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f58,axiom,(
% 0.12/0.42 genls(c_tptpcol_14_72792,c_tptpcol_13_72791) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f60,axiom,(
% 0.12/0.42 genls(c_tptpcol_15_72793,c_tptpcol_14_72792) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f62,axiom,(
% 0.12/0.42 genls(c_tptpcol_16_72795,c_tptpcol_15_72793) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f64,axiom,(
% 0.12/0.42 disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f84,axiom,(
% 0.12/0.42 (! [ARG1,OLD,NEW] :( ( disjointwith(ARG1,OLD)& genls(NEW,OLD) )=> disjointwith(ARG1,NEW) ) )),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f85,axiom,(
% 0.12/0.42 (! [OLD,ARG2,NEW] :( ( disjointwith(OLD,ARG2)& genls(NEW,OLD) )=> disjointwith(NEW,ARG2) ) )),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f152,axiom,(
% 0.12/0.42 (! [X,Y,Z] :( ( genls(X,Y)& genls(Y,Z) )=> genls(X,Z) ) )),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f174,conjecture,(
% 0.12/0.42 ( mtvisible(c_tptp_member974_mt)=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ) ),
% 0.12/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.42 fof(f175,negated_conjecture,(
% 0.12/0.42 ~(( mtvisible(c_tptp_member974_mt)=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ) )),
% 0.12/0.42 inference(negated_conjecture,[status(cth)],[f174])).
% 0.12/0.42 fof(f181,plain,(
% 0.12/0.42 genls(c_tptpcol_2_2,c_tptpcol_1_1)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f6])).
% 0.12/0.42 fof(f184,plain,(
% 0.12/0.42 genls(c_tptpcol_3_16386,c_tptpcol_2_2)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/0.42 fof(f187,plain,(
% 0.12/0.42 genls(c_tptpcol_4_16387,c_tptpcol_3_16386)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f10])).
% 0.12/0.42 fof(f190,plain,(
% 0.12/0.42 genls(c_tptpcol_5_20483,c_tptpcol_4_16387)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f12])).
% 0.12/0.42 fof(f193,plain,(
% 0.12/0.42 genls(c_tptpcol_6_20484,c_tptpcol_5_20483)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f14])).
% 0.12/0.42 fof(f196,plain,(
% 0.12/0.42 genls(c_tptpcol_7_21508,c_tptpcol_6_20484)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f16])).
% 0.12/0.42 fof(f199,plain,(
% 0.12/0.42 genls(c_tptpcol_8_22020,c_tptpcol_7_21508)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f18])).
% 0.12/0.42 fof(f202,plain,(
% 0.12/0.42 genls(c_tptpcol_9_22021,c_tptpcol_8_22020)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f20])).
% 0.12/0.42 fof(f205,plain,(
% 0.12/0.42 genls(c_tptpcol_10_22022,c_tptpcol_9_22021)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f22])).
% 0.12/0.42 fof(f208,plain,(
% 0.12/0.42 genls(c_tptpcol_11_22023,c_tptpcol_10_22022)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f24])).
% 0.12/0.42 fof(f211,plain,(
% 0.12/0.42 genls(c_tptpcol_12_22055,c_tptpcol_11_22023)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f26])).
% 0.12/0.42 fof(f214,plain,(
% 0.12/0.42 genls(c_tptpcol_13_22071,c_tptpcol_12_22055)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f28])).
% 0.12/0.42 fof(f217,plain,(
% 0.12/0.42 genls(c_tptpcol_14_22072,c_tptpcol_13_22071)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f30])).
% 0.12/0.42 fof(f220,plain,(
% 0.12/0.42 genls(c_tptpcol_15_22076,c_tptpcol_14_22072)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f32])).
% 0.12/0.42 fof(f223,plain,(
% 0.12/0.42 genls(c_tptpcol_2_65537,c_tptpcol_1_65536)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f34])).
% 0.12/0.42 fof(f226,plain,(
% 0.12/0.42 genls(c_tptpcol_3_65538,c_tptpcol_2_65537)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f36])).
% 0.12/0.42 fof(f229,plain,(
% 0.12/0.42 genls(c_tptpcol_4_65539,c_tptpcol_3_65538)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f38])).
% 0.12/0.42 fof(f232,plain,(
% 0.12/0.42 genls(c_tptpcol_5_69635,c_tptpcol_4_65539)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f40])).
% 0.12/0.42 fof(f235,plain,(
% 0.12/0.42 genls(c_tptpcol_6_71683,c_tptpcol_5_69635)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.42 fof(f238,plain,(
% 0.12/0.42 genls(c_tptpcol_7_72707,c_tptpcol_6_71683)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f44])).
% 0.12/0.42 fof(f241,plain,(
% 0.12/0.42 genls(c_tptpcol_8_72708,c_tptpcol_7_72707)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f46])).
% 0.12/0.42 fof(f244,plain,(
% 0.12/0.42 genls(c_tptpcol_9_72709,c_tptpcol_8_72708)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f48])).
% 0.12/0.42 fof(f247,plain,(
% 0.12/0.42 genls(c_tptpcol_10_72710,c_tptpcol_9_72709)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f50])).
% 0.12/0.42 fof(f250,plain,(
% 0.12/0.42 genls(c_tptpcol_11_72774,c_tptpcol_10_72710)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f52])).
% 0.12/0.42 fof(f253,plain,(
% 0.12/0.42 genls(c_tptpcol_12_72775,c_tptpcol_11_72774)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f54])).
% 0.12/0.42 fof(f256,plain,(
% 0.12/0.42 genls(c_tptpcol_13_72791,c_tptpcol_12_72775)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f56])).
% 0.12/0.42 fof(f259,plain,(
% 0.12/0.42 genls(c_tptpcol_14_72792,c_tptpcol_13_72791)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f58])).
% 0.12/0.42 fof(f262,plain,(
% 0.12/0.42 genls(c_tptpcol_15_72793,c_tptpcol_14_72792)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f60])).
% 0.12/0.42 fof(f265,plain,(
% 0.12/0.42 genls(c_tptpcol_16_72795,c_tptpcol_15_72793)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f62])).
% 0.12/0.42 fof(f268,plain,(
% 0.12/0.42 disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f64])).
% 0.12/0.42 fof(f318,plain,(
% 0.12/0.42 ![ARG1,OLD,NEW]: ((~disjointwith(ARG1,OLD)|~genls(NEW,OLD))|disjointwith(ARG1,NEW))),
% 0.12/0.42 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 0.12/0.42 fof(f319,plain,(
% 0.12/0.42 ![ARG1,NEW]: ((![OLD]: (~disjointwith(ARG1,OLD)|~genls(NEW,OLD)))|disjointwith(ARG1,NEW))),
% 0.12/0.42 inference(miniscoping,[status(thm)],[f318])).
% 0.12/0.42 fof(f320,plain,(
% 0.12/0.42 ![X0,X1,X2]: (~disjointwith(X0,X1)|~genls(X2,X1)|disjointwith(X0,X2))),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f319])).
% 0.12/0.42 fof(f321,plain,(
% 0.12/0.42 ![OLD,ARG2,NEW]: ((~disjointwith(OLD,ARG2)|~genls(NEW,OLD))|disjointwith(NEW,ARG2))),
% 0.12/0.42 inference(pre_NNF_transformation,[status(thm)],[f85])).
% 0.12/0.42 fof(f322,plain,(
% 0.12/0.42 ![ARG2,NEW]: ((![OLD]: (~disjointwith(OLD,ARG2)|~genls(NEW,OLD)))|disjointwith(NEW,ARG2))),
% 0.12/0.42 inference(miniscoping,[status(thm)],[f321])).
% 0.12/0.42 fof(f323,plain,(
% 0.12/0.42 ![X0,X1,X2]: (~disjointwith(X0,X1)|~genls(X2,X0)|disjointwith(X2,X1))),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f322])).
% 0.12/0.42 fof(f460,plain,(
% 0.12/0.42 ![X,Y,Z]: ((~genls(X,Y)|~genls(Y,Z))|genls(X,Z))),
% 0.12/0.42 inference(pre_NNF_transformation,[status(thm)],[f152])).
% 0.12/0.42 fof(f461,plain,(
% 0.12/0.42 ![X,Z]: ((![Y]: (~genls(X,Y)|~genls(Y,Z)))|genls(X,Z))),
% 0.12/0.42 inference(miniscoping,[status(thm)],[f460])).
% 0.12/0.42 fof(f462,plain,(
% 0.12/0.42 ![X0,X1,X2]: (~genls(X0,X1)|~genls(X1,X2)|genls(X0,X2))),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f461])).
% 0.12/0.42 fof(f516,plain,(
% 0.12/0.42 (mtvisible(c_tptp_member974_mt)&~disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795))),
% 0.12/0.42 inference(pre_NNF_transformation,[status(thm)],[f175])).
% 0.12/0.42 fof(f518,plain,(
% 0.12/0.42 ~disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)),
% 0.12/0.42 inference(cnf_transformation,[status(thm)],[f516])).
% 0.12/0.42 fof(f525,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_1_1)|disjointwith(X0,c_tptpcol_1_65536))),
% 0.12/0.42 inference(resolution,[status(thm)],[f268,f323])).
% 0.12/0.42 fof(f528,plain,(
% 0.12/0.42 disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536)),
% 0.12/0.42 inference(resolution,[status(thm)],[f525,f181])).
% 0.12/0.42 fof(f546,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_2_2)|disjointwith(X0,c_tptpcol_1_65536))),
% 0.12/0.42 inference(resolution,[status(thm)],[f528,f323])).
% 0.12/0.42 fof(f557,plain,(
% 0.12/0.42 disjointwith(c_tptpcol_3_16386,c_tptpcol_1_65536)),
% 0.12/0.42 inference(resolution,[status(thm)],[f546,f184])).
% 0.12/0.42 fof(f573,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_3_16386)|disjointwith(X0,c_tptpcol_1_65536))),
% 0.12/0.42 inference(resolution,[status(thm)],[f557,f323])).
% 0.12/0.42 fof(f595,plain,(
% 0.12/0.42 disjointwith(c_tptpcol_4_16387,c_tptpcol_1_65536)),
% 0.12/0.42 inference(resolution,[status(thm)],[f573,f187])).
% 0.12/0.42 fof(f609,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_4_16387)|disjointwith(X0,c_tptpcol_1_65536))),
% 0.12/0.42 inference(resolution,[status(thm)],[f595,f323])).
% 0.12/0.42 fof(f657,plain,(
% 0.12/0.42 disjointwith(c_tptpcol_5_20483,c_tptpcol_1_65536)),
% 0.12/0.42 inference(resolution,[status(thm)],[f609,f190])).
% 0.12/0.42 fof(f661,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_5_20483)|disjointwith(X0,c_tptpcol_1_65536))),
% 0.12/0.42 inference(resolution,[status(thm)],[f657,f323])).
% 0.12/0.42 fof(f830,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_15_72793)|genls(X0,c_tptpcol_14_72792))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f262])).
% 0.12/0.42 fof(f831,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_14_72792)|genls(X0,c_tptpcol_13_72791))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f259])).
% 0.12/0.42 fof(f832,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_13_72791)|genls(X0,c_tptpcol_12_72775))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f256])).
% 0.12/0.42 fof(f833,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_12_72775)|genls(X0,c_tptpcol_11_72774))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f253])).
% 0.12/0.42 fof(f834,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_11_72774)|genls(X0,c_tptpcol_10_72710))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f250])).
% 0.12/0.42 fof(f835,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_10_72710)|genls(X0,c_tptpcol_9_72709))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f247])).
% 0.12/0.42 fof(f836,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_9_72709)|genls(X0,c_tptpcol_8_72708))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f244])).
% 0.12/0.42 fof(f837,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_8_72708)|genls(X0,c_tptpcol_7_72707))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f241])).
% 0.12/0.42 fof(f838,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_7_72707)|genls(X0,c_tptpcol_6_71683))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f238])).
% 0.12/0.42 fof(f839,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_6_71683)|genls(X0,c_tptpcol_5_69635))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f235])).
% 0.12/0.42 fof(f840,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_5_69635)|genls(X0,c_tptpcol_4_65539))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f232])).
% 0.12/0.42 fof(f841,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_4_65539)|genls(X0,c_tptpcol_3_65538))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f229])).
% 0.12/0.42 fof(f842,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_3_65538)|genls(X0,c_tptpcol_2_65537))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f226])).
% 0.12/0.42 fof(f843,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_2_65537)|genls(X0,c_tptpcol_1_65536))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f223])).
% 0.12/0.42 fof(f844,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_14_22072)|genls(X0,c_tptpcol_13_22071))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f217])).
% 0.12/0.42 fof(f845,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_13_22071)|genls(X0,c_tptpcol_12_22055))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f214])).
% 0.12/0.42 fof(f846,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_12_22055)|genls(X0,c_tptpcol_11_22023))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f211])).
% 0.12/0.42 fof(f847,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_11_22023)|genls(X0,c_tptpcol_10_22022))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f208])).
% 0.12/0.42 fof(f848,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_10_22022)|genls(X0,c_tptpcol_9_22021))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f205])).
% 0.12/0.42 fof(f849,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_9_22021)|genls(X0,c_tptpcol_8_22020))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f202])).
% 0.12/0.42 fof(f850,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_8_22020)|genls(X0,c_tptpcol_7_21508))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f199])).
% 0.12/0.42 fof(f851,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_7_21508)|genls(X0,c_tptpcol_6_20484))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f196])).
% 0.12/0.42 fof(f852,plain,(
% 0.12/0.42 ![X0]: (~genls(X0,c_tptpcol_6_20484)|genls(X0,c_tptpcol_5_20483))),
% 0.12/0.42 inference(resolution,[status(thm)],[f462,f193])).
% 0.12/0.42 fof(f1016,plain,(
% 0.12/0.42 genls(c_tptpcol_16_72795,c_tptpcol_14_72792)),
% 0.12/0.42 inference(resolution,[status(thm)],[f830,f265])).
% 0.12/0.42 fof(f1027,plain,(
% 0.12/0.42 genls(c_tptpcol_16_72795,c_tptpcol_13_72791)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1016,f831])).
% 0.12/0.42 fof(f1031,plain,(
% 0.12/0.42 genls(c_tptpcol_16_72795,c_tptpcol_12_72775)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1027,f832])).
% 0.12/0.42 fof(f1050,plain,(
% 0.12/0.42 genls(c_tptpcol_16_72795,c_tptpcol_11_72774)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1031,f833])).
% 0.12/0.42 fof(f1055,plain,(
% 0.12/0.42 genls(c_tptpcol_16_72795,c_tptpcol_10_72710)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1050,f834])).
% 0.12/0.42 fof(f1072,plain,(
% 0.12/0.42 genls(c_tptpcol_16_72795,c_tptpcol_9_72709)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1055,f835])).
% 0.12/0.42 fof(f1078,plain,(
% 0.12/0.42 genls(c_tptpcol_16_72795,c_tptpcol_8_72708)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1072,f836])).
% 0.12/0.42 fof(f1082,plain,(
% 0.12/0.42 genls(c_tptpcol_16_72795,c_tptpcol_7_72707)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1078,f837])).
% 0.12/0.42 fof(f1088,plain,(
% 0.12/0.42 genls(c_tptpcol_16_72795,c_tptpcol_6_71683)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1082,f838])).
% 0.12/0.42 fof(f1107,plain,(
% 0.12/0.42 genls(c_tptpcol_15_22076,c_tptpcol_13_22071)),
% 0.12/0.42 inference(resolution,[status(thm)],[f844,f220])).
% 0.12/0.42 fof(f1113,plain,(
% 0.12/0.42 genls(c_tptpcol_16_72795,c_tptpcol_5_69635)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1088,f839])).
% 0.12/0.42 fof(f1117,plain,(
% 0.12/0.42 genls(c_tptpcol_15_22076,c_tptpcol_12_22055)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1107,f845])).
% 0.12/0.42 fof(f1121,plain,(
% 0.12/0.42 genls(c_tptpcol_15_22076,c_tptpcol_11_22023)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1117,f846])).
% 0.12/0.42 fof(f1125,plain,(
% 0.12/0.42 genls(c_tptpcol_16_72795,c_tptpcol_4_65539)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1113,f840])).
% 0.12/0.42 fof(f1131,plain,(
% 0.12/0.42 genls(c_tptpcol_15_22076,c_tptpcol_10_22022)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1121,f847])).
% 0.12/0.42 fof(f1155,plain,(
% 0.12/0.42 genls(c_tptpcol_15_22076,c_tptpcol_9_22021)),
% 0.12/0.42 inference(resolution,[status(thm)],[f848,f1131])).
% 0.12/0.42 fof(f1163,plain,(
% 0.12/0.42 genls(c_tptpcol_16_72795,c_tptpcol_3_65538)),
% 0.12/0.42 inference(resolution,[status(thm)],[f1125,f841])).
% 0.12/0.43 fof(f1172,plain,(
% 0.12/0.43 genls(c_tptpcol_15_22076,c_tptpcol_8_22020)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1155,f849])).
% 0.12/0.43 fof(f1186,plain,(
% 0.12/0.43 genls(c_tptpcol_15_22076,c_tptpcol_7_21508)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1172,f850])).
% 0.12/0.43 fof(f1191,plain,(
% 0.12/0.43 genls(c_tptpcol_15_22076,c_tptpcol_6_20484)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1186,f851])).
% 0.12/0.43 fof(f1222,plain,(
% 0.12/0.43 genls(c_tptpcol_16_72795,c_tptpcol_2_65537)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1163,f842])).
% 0.12/0.43 fof(f1247,plain,(
% 0.12/0.43 genls(c_tptpcol_15_22076,c_tptpcol_5_20483)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1191,f852])).
% 0.12/0.43 fof(f1274,plain,(
% 0.12/0.43 genls(c_tptpcol_16_72795,c_tptpcol_1_65536)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1222,f843])).
% 0.12/0.43 fof(f1376,plain,(
% 0.12/0.43 disjointwith(c_tptpcol_15_22076,c_tptpcol_1_65536)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1247,f661])).
% 0.12/0.43 fof(f1553,plain,(
% 0.12/0.43 ![X0]: (~genls(X0,c_tptpcol_1_65536)|disjointwith(c_tptpcol_15_22076,X0))),
% 0.12/0.43 inference(resolution,[status(thm)],[f1376,f320])).
% 0.12/0.43 fof(f2114,plain,(
% 0.12/0.43 disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)),
% 0.12/0.43 inference(resolution,[status(thm)],[f1553,f1274])).
% 0.12/0.43 fof(f2115,plain,(
% 0.12/0.43 $false),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f2114,f518])).
% 0.12/0.43 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.44 % Elapsed time: 0.087657 seconds
% 0.12/0.44 % CPU time: 0.407500 seconds
% 0.12/0.44 % Total memory used: 67.913 MB
% 0.12/0.44 % Net memory used: 67.364 MB
%------------------------------------------------------------------------------