%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR061+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 : n018.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:55 PM UTC 2026
% Result : Theorem 3.01s 0.85s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR061+2 : 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.10/0.35 % Computer : n018.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 14:42:29 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.12/0.39 % Drodi V4.1.1
% 3.01/0.85 % Refutation found
% 3.01/0.85 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.01/0.85 % SZS output start CNFRefutation for theBenchmark
% 3.01/0.85 fof(f68,axiom,(
% 3.01/0.85 genls(c_tptpcol_4_106497,c_tptpcol_3_98305) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f70,axiom,(
% 3.01/0.85 genls(c_tptpcol_5_114690,c_tptpcol_4_114689) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f100,axiom,(
% 3.01/0.85 genls(c_tptpcol_6_116738,c_tptpcol_5_114690) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f129,axiom,(
% 3.01/0.85 genls(c_tptpcol_11_118084,c_tptpcol_10_118020) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f160,axiom,(
% 3.01/0.85 genls(c_tptpcol_10_118020,c_tptpcol_9_118019) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f215,axiom,(
% 3.01/0.85 genls(c_tptpcol_7_113665,c_tptpcol_6_112641) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f235,axiom,(
% 3.01/0.85 genls(c_tptpcol_4_114689,c_tptpcol_3_114688) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f258,axiom,(
% 3.01/0.85 genls(c_tptpcol_12_118116,c_tptpcol_11_118084) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f356,axiom,(
% 3.01/0.85 genls(c_tptpcol_8_117763,c_tptpcol_7_117762) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f361,axiom,(
% 3.01/0.85 genls(c_tptpcol_7_117762,c_tptpcol_6_116738) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f387,axiom,(
% 3.01/0.85 genls(c_tptpcol_9_118019,c_tptpcol_8_117763) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f393,axiom,(
% 3.01/0.85 genls(c_tptpcol_6_112641,c_tptpcol_5_110593) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f401,axiom,(
% 3.01/0.85 genls(c_tptpcol_8_114177,c_tptpcol_7_113665) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f422,axiom,(
% 3.01/0.85 genls(c_tptpcol_13_118117,c_tptpcol_12_118116) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f487,axiom,(
% 3.01/0.85 disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f489,axiom,(
% 3.01/0.85 genls(c_tptpcol_5_110593,c_tptpcol_4_106497) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f499,axiom,(
% 3.01/0.85 genls(c_tptpcol_14_118118,c_tptpcol_13_118117) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f1121,axiom,(
% 3.01/0.85 (! [ARG1,OLD,NEW] :( ( disjointwith(ARG1,OLD)& genls(NEW,OLD) )=> disjointwith(ARG1,NEW) ) )),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f1122,axiom,(
% 3.01/0.85 (! [OLD,ARG2,NEW] :( ( disjointwith(OLD,ARG2)& genls(NEW,OLD) )=> disjointwith(NEW,ARG2) ) )),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f1132,conjecture,(
% 3.01/0.85 ( mtvisible(c_timehasnoendmt)=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ) ),
% 3.01/0.85 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.01/0.85 fof(f1133,negated_conjecture,(
% 3.01/0.85 ~(( mtvisible(c_timehasnoendmt)=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ) )),
% 3.01/0.85 inference(negated_conjecture,[status(cth)],[f1132])).
% 3.01/0.85 fof(f1231,plain,(
% 3.01/0.85 genls(c_tptpcol_4_106497,c_tptpcol_3_98305)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f68])).
% 3.01/0.85 fof(f1234,plain,(
% 3.01/0.85 genls(c_tptpcol_5_114690,c_tptpcol_4_114689)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f70])).
% 3.01/0.85 fof(f1277,plain,(
% 3.01/0.85 genls(c_tptpcol_6_116738,c_tptpcol_5_114690)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f100])).
% 3.01/0.85 fof(f1322,plain,(
% 3.01/0.85 genls(c_tptpcol_11_118084,c_tptpcol_10_118020)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f129])).
% 3.01/0.85 fof(f1366,plain,(
% 3.01/0.85 genls(c_tptpcol_10_118020,c_tptpcol_9_118019)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f160])).
% 3.01/0.85 fof(f1447,plain,(
% 3.01/0.85 genls(c_tptpcol_7_113665,c_tptpcol_6_112641)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f215])).
% 3.01/0.85 fof(f1477,plain,(
% 3.01/0.85 genls(c_tptpcol_4_114689,c_tptpcol_3_114688)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f235])).
% 3.01/0.85 fof(f1509,plain,(
% 3.01/0.85 genls(c_tptpcol_12_118116,c_tptpcol_11_118084)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f258])).
% 3.01/0.85 fof(f1652,plain,(
% 3.01/0.85 genls(c_tptpcol_8_117763,c_tptpcol_7_117762)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f356])).
% 3.01/0.85 fof(f1659,plain,(
% 3.01/0.85 genls(c_tptpcol_7_117762,c_tptpcol_6_116738)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f361])).
% 3.01/0.85 fof(f1697,plain,(
% 3.01/0.85 genls(c_tptpcol_9_118019,c_tptpcol_8_117763)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f387])).
% 3.01/0.85 fof(f1706,plain,(
% 3.01/0.85 genls(c_tptpcol_6_112641,c_tptpcol_5_110593)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f393])).
% 3.01/0.85 fof(f1718,plain,(
% 3.01/0.85 genls(c_tptpcol_8_114177,c_tptpcol_7_113665)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f401])).
% 3.01/0.85 fof(f1748,plain,(
% 3.01/0.85 genls(c_tptpcol_13_118117,c_tptpcol_12_118116)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f422])).
% 3.01/0.85 fof(f1846,plain,(
% 3.01/0.85 disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f487])).
% 3.01/0.85 fof(f1849,plain,(
% 3.01/0.85 genls(c_tptpcol_5_110593,c_tptpcol_4_106497)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f489])).
% 3.01/0.85 fof(f1865,plain,(
% 3.01/0.85 genls(c_tptpcol_14_118118,c_tptpcol_13_118117)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f499])).
% 3.01/0.85 fof(f3175,plain,(
% 3.01/0.85 ![ARG1,OLD,NEW]: ((~disjointwith(ARG1,OLD)|~genls(NEW,OLD))|disjointwith(ARG1,NEW))),
% 3.01/0.85 inference(pre_NNF_transformation,[status(thm)],[f1121])).
% 3.01/0.85 fof(f3176,plain,(
% 3.01/0.85 ![ARG1,NEW]: ((![OLD]: (~disjointwith(ARG1,OLD)|~genls(NEW,OLD)))|disjointwith(ARG1,NEW))),
% 3.01/0.85 inference(miniscoping,[status(thm)],[f3175])).
% 3.01/0.85 fof(f3177,plain,(
% 3.01/0.85 ![X0,X1,X2]: (~disjointwith(X0,X1)|~genls(X2,X1)|disjointwith(X0,X2))),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f3176])).
% 3.01/0.85 fof(f3178,plain,(
% 3.01/0.85 ![OLD,ARG2,NEW]: ((~disjointwith(OLD,ARG2)|~genls(NEW,OLD))|disjointwith(NEW,ARG2))),
% 3.01/0.85 inference(pre_NNF_transformation,[status(thm)],[f1122])).
% 3.01/0.85 fof(f3179,plain,(
% 3.01/0.85 ![ARG2,NEW]: ((![OLD]: (~disjointwith(OLD,ARG2)|~genls(NEW,OLD)))|disjointwith(NEW,ARG2))),
% 3.01/0.85 inference(miniscoping,[status(thm)],[f3178])).
% 3.01/0.85 fof(f3180,plain,(
% 3.01/0.85 ![X0,X1,X2]: (~disjointwith(X0,X1)|~genls(X2,X0)|disjointwith(X2,X1))),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f3179])).
% 3.01/0.85 fof(f3204,plain,(
% 3.01/0.85 (mtvisible(c_timehasnoendmt)&~disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118))),
% 3.01/0.85 inference(pre_NNF_transformation,[status(thm)],[f1133])).
% 3.01/0.85 fof(f3206,plain,(
% 3.01/0.85 ~disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118)),
% 3.01/0.85 inference(cnf_transformation,[status(thm)],[f3204])).
% 3.01/0.85 fof(f5898,plain,(
% 3.01/0.85 ![X0]: (~disjointwith(c_tptpcol_8_114177,X0)|~genls(c_tptpcol_14_118118,X0))),
% 3.01/0.85 inference(resolution,[status(thm)],[f3177,f3206])).
% 3.01/0.85 fof(f6199,plain,(
% 3.01/0.85 ![X0,X1]: (~genls(c_tptpcol_14_118118,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_8_114177,X1))),
% 3.01/0.85 inference(resolution,[status(thm)],[f5898,f3180])).
% 3.01/0.85 fof(f6843,plain,(
% 3.01/0.85 ![X0]: (~disjointwith(X0,c_tptpcol_13_118117)|~genls(c_tptpcol_8_114177,X0))),
% 3.01/0.85 inference(resolution,[status(thm)],[f6199,f1865])).
% 3.01/0.85 fof(f6847,plain,(
% 3.01/0.85 ![X0,X1]: (~genls(c_tptpcol_8_114177,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_13_118117,X1))),
% 3.01/0.85 inference(resolution,[status(thm)],[f6843,f3177])).
% 3.01/0.85 fof(f6911,plain,(
% 3.01/0.85 ![X0]: (~genls(c_tptpcol_8_114177,X0)|~disjointwith(X0,c_tptpcol_12_118116))),
% 3.01/0.85 inference(resolution,[status(thm)],[f6847,f1748])).
% 3.01/0.85 fof(f6915,plain,(
% 3.01/0.85 ![X0,X1]: (~genls(c_tptpcol_8_114177,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_12_118116,X1))),
% 3.01/0.85 inference(resolution,[status(thm)],[f6911,f3177])).
% 3.01/0.85 fof(f6929,plain,(
% 3.01/0.85 ![X0]: (~disjointwith(c_tptpcol_7_113665,X0)|~genls(c_tptpcol_12_118116,X0))),
% 3.01/0.85 inference(resolution,[status(thm)],[f6915,f1718])).
% 3.01/0.85 fof(f6933,plain,(
% 3.01/0.85 ![X0,X1]: (~genls(c_tptpcol_12_118116,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_7_113665,X1))),
% 3.01/0.85 inference(resolution,[status(thm)],[f6929,f3180])).
% 3.01/0.85 fof(f6951,plain,(
% 3.01/0.85 ![X0]: (~disjointwith(X0,c_tptpcol_11_118084)|~genls(c_tptpcol_7_113665,X0))),
% 3.01/0.85 inference(resolution,[status(thm)],[f6933,f1509])).
% 3.01/0.85 fof(f6956,plain,(
% 3.01/0.85 ![X0,X1]: (~genls(c_tptpcol_7_113665,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_11_118084,X1))),
% 3.01/0.85 inference(resolution,[status(thm)],[f6951,f3177])).
% 3.01/0.85 fof(f6985,plain,(
% 3.01/0.85 ![X0]: (~disjointwith(c_tptpcol_6_112641,X0)|~genls(c_tptpcol_11_118084,X0))),
% 3.01/0.85 inference(resolution,[status(thm)],[f6956,f1447])).
% 3.01/0.85 fof(f6989,plain,(
% 3.01/0.85 ![X0,X1]: (~genls(c_tptpcol_11_118084,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_6_112641,X1))),
% 3.01/0.88 inference(resolution,[status(thm)],[f6985,f3180])).
% 3.01/0.88 fof(f7013,plain,(
% 3.01/0.88 ![X0]: (~genls(c_tptpcol_11_118084,X0)|~disjointwith(c_tptpcol_5_110593,X0))),
% 3.01/0.88 inference(resolution,[status(thm)],[f6989,f1706])).
% 3.01/0.88 fof(f7016,plain,(
% 3.01/0.88 ![X0,X1]: (~genls(c_tptpcol_11_118084,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_5_110593,X1))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7013,f3180])).
% 3.01/0.88 fof(f7037,plain,(
% 3.01/0.88 ![X0]: (~genls(c_tptpcol_11_118084,X0)|~disjointwith(c_tptpcol_4_106497,X0))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7016,f1849])).
% 3.01/0.88 fof(f7040,plain,(
% 3.01/0.88 ![X0,X1]: (~genls(c_tptpcol_11_118084,X0)|~disjointwith(X1,X0)|~genls(c_tptpcol_4_106497,X1))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7037,f3180])).
% 3.01/0.88 fof(f7055,plain,(
% 3.01/0.88 ![X0]: (~disjointwith(X0,c_tptpcol_10_118020)|~genls(c_tptpcol_4_106497,X0))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7040,f1322])).
% 3.01/0.88 fof(f7060,plain,(
% 3.01/0.88 ![X0,X1]: (~genls(c_tptpcol_4_106497,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_10_118020,X1))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7055,f3177])).
% 3.01/0.88 fof(f7083,plain,(
% 3.01/0.88 ![X0]: (~genls(c_tptpcol_4_106497,X0)|~disjointwith(X0,c_tptpcol_9_118019))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7060,f1366])).
% 3.01/0.88 fof(f7087,plain,(
% 3.01/0.88 ![X0,X1]: (~genls(c_tptpcol_4_106497,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_9_118019,X1))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7083,f3177])).
% 3.01/0.88 fof(f7107,plain,(
% 3.01/0.88 ![X0]: (~genls(c_tptpcol_4_106497,X0)|~disjointwith(X0,c_tptpcol_8_117763))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7087,f1697])).
% 3.01/0.88 fof(f7111,plain,(
% 3.01/0.88 ![X0,X1]: (~genls(c_tptpcol_4_106497,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_8_117763,X1))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7107,f3177])).
% 3.01/0.88 fof(f7125,plain,(
% 3.01/0.88 ![X0]: (~genls(c_tptpcol_4_106497,X0)|~disjointwith(X0,c_tptpcol_7_117762))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7111,f1652])).
% 3.01/0.88 fof(f7129,plain,(
% 3.01/0.88 ![X0,X1]: (~genls(c_tptpcol_4_106497,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_7_117762,X1))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7125,f3177])).
% 3.01/0.88 fof(f7143,plain,(
% 3.01/0.88 ![X0]: (~genls(c_tptpcol_4_106497,X0)|~disjointwith(X0,c_tptpcol_6_116738))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7129,f1659])).
% 3.01/0.88 fof(f7147,plain,(
% 3.01/0.88 ![X0,X1]: (~genls(c_tptpcol_4_106497,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_6_116738,X1))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7143,f3177])).
% 3.01/0.88 fof(f7161,plain,(
% 3.01/0.88 ![X0]: (~genls(c_tptpcol_4_106497,X0)|~disjointwith(X0,c_tptpcol_5_114690))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7147,f1277])).
% 3.01/0.88 fof(f7165,plain,(
% 3.01/0.88 ![X0,X1]: (~genls(c_tptpcol_4_106497,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_5_114690,X1))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7161,f3177])).
% 3.01/0.88 fof(f7179,plain,(
% 3.01/0.88 ![X0]: (~genls(c_tptpcol_4_106497,X0)|~disjointwith(X0,c_tptpcol_4_114689))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7165,f1234])).
% 3.01/0.88 fof(f7183,plain,(
% 3.01/0.88 ![X0,X1]: (~genls(c_tptpcol_4_106497,X0)|~disjointwith(X0,X1)|~genls(c_tptpcol_4_114689,X1))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7179,f3177])).
% 3.01/0.88 fof(f7197,plain,(
% 3.01/0.88 ![X0]: (~genls(c_tptpcol_4_106497,X0)|~disjointwith(X0,c_tptpcol_3_114688))),
% 3.01/0.88 inference(resolution,[status(thm)],[f7183,f1477])).
% 3.01/0.88 fof(f7200,plain,(
% 3.01/0.88 ~disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688)),
% 3.01/0.88 inference(resolution,[status(thm)],[f7197,f1231])).
% 3.01/0.88 fof(f7203,plain,(
% 3.01/0.88 $false),
% 3.01/0.88 inference(forward_subsumption_resolution,[status(thm)],[f7200,f1846])).
% 3.01/0.88 % SZS output end CNFRefutation for theBenchmark.p
% 2.26/2.09 % Elapsed time: 1.513133 seconds
% 2.26/2.09 % CPU time: 3.505515 seconds
% 2.26/2.09 % Total memory used: 180.588 MB
% 2.26/2.09 % Net memory used: 177.776 MB
%------------------------------------------------------------------------------