%------------------------------------------------------------------------------
% File : Toma---0.7
% Problem : CSR039-10 : TPTP v9.0.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_Leo-III %s %d THM
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Jul 15 06:29:04 AM UTC 2025
% Result : Unsatisfiable 77.11s 77.18s
% Output : CNFRefutation 77.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 34
% Syntax : Number of clauses : 92 ( 92 unt; 0 nHn; 61 RR)
% Number of literals : 92 ( 91 equ; 1 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 31 con; 0-4 aty)
% Number of variables : 40 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(g0,negated_conjecture,
a != b,
file('theBenchmark.p',goal) ).
cnf(c31,axiom,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436) = true,
file('theBenchmark.p',ax1_483) ).
cnf(c40,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113) = true,
file('theBenchmark.p',ax1_476) ).
cnf(c45,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114) = true,
file('theBenchmark.p',ax1_417) ).
cnf(c46,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2) = true,
file('theBenchmark.p',ax1_385) ).
cnf(c95,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386) = true,
file('theBenchmark.p',ax1_285) ).
cnf(c100,axiom,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438) = true,
file('theBenchmark.p',ax1_255) ).
cnf(c115,axiom,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186) = true,
file('theBenchmark.p',ax1_345) ).
cnf(c116,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536) = true,
file('theBenchmark.p',ax1_348) ).
cnf(c117,axiom,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388) = true,
file('theBenchmark.p',ax1_351) ).
cnf(c121,axiom,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437) = true,
file('theBenchmark.p',ax1_353) ).
cnf(c129,axiom,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698) = true,
file('theBenchmark.p',ax1_370) ).
cnf(c130,axiom,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700) = true,
file('theBenchmark.p',ax1_372) ).
cnf(c131,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921) = true,
file('theBenchmark.p',ax1_376) ).
cnf(c134,axiom,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699) = true,
file('theBenchmark.p',ax1_379) ).
cnf(c169,axiom,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663) = true,
file('theBenchmark.p',ax1_208) ).
cnf(c179,axiom,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766) = true,
file('theBenchmark.p',ax1_191) ).
cnf(c184,axiom,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567) = true,
file('theBenchmark.p',ax1_175) ).
cnf(c188,axiom,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774) = true,
file('theBenchmark.p',ax1_182) ).
cnf(c194,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1) = true,
file('theBenchmark.p',ax1_145) ).
cnf(c199,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) = true,
file('theBenchmark.p',ax1_152) ).
cnf(c215,axiom,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631) = true,
file('theBenchmark.p',ax1_109) ).
cnf(c225,axiom,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765) = true,
file('theBenchmark.p',ax1_78) ).
cnf(c226,axiom,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764) = true,
file('theBenchmark.p',ax1_72) ).
cnf(c232,axiom,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162) = true,
file('theBenchmark.p',ax1_14) ).
cnf(c253,axiom,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387) = true,
file('theBenchmark.p',ax1_23) ).
cnf(c260,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537) = true,
file('theBenchmark.p',ax1_41) ).
cnf(c263,axiom,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439) = true,
file('theBenchmark.p',ax1_43) ).
cnf(c284,axiom,
ifeq3(X,X,Y,Z) = Y,
file('theBenchmark.p',ifeq_axiom_001) ).
cnf(c286,axiom,
ifeq4(X,X,Y,Z) = Y,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c538,axiom,
ifeq3(disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),true,a,b) = b,
file('theBenchmark.p',query89_1) ).
cnf(c5065,axiom,
ifeq4(disjointwith(X,Y),true,disjointwith(Y,X),true) = true,
file('theBenchmark.p',ax1_1120) ).
cnf(c5069,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1) = true,
inference(equational,[status(thm)],[c199,c286,c5065]) ).
cnf(c18634,axiom,
ifeq4(genls(X,Y),true,ifeq4(disjointwith(Y,Z),true,disjointwith(X,Z),true),true) = true,
file('theBenchmark.p',ax1_1122) ).
cnf(c19129,plain,
ifeq4(disjointwith(c_tptpcol_1_65536,X),true,disjointwith(c_tptpcol_2_65537,X),true) = true,
inference(equational,[status(thm)],[c116,c286,c18634]) ).
cnf(c19130,plain,
disjointwith(c_tptpcol_2_65537,c_tptpcol_1_1) = true,
inference(equational,[status(thm)],[c286,c5069,c19129]) ).
cnf(c19554,plain,
ifeq4(disjointwith(c_tptpcol_2_65537,X),true,disjointwith(c_tptpcol_3_81921,X),true) = true,
inference(equational,[status(thm)],[c260,c286,c18634]) ).
cnf(c19555,plain,
disjointwith(c_tptpcol_3_81921,c_tptpcol_1_1) = true,
inference(equational,[status(thm)],[c286,c19130,c19554]) ).
cnf(c19908,plain,
ifeq4(disjointwith(c_tptpcol_3_81921,X),true,disjointwith(c_tptpcol_4_90113,X),true) = true,
inference(equational,[status(thm)],[c131,c286,c18634]) ).
cnf(c19909,plain,
disjointwith(c_tptpcol_4_90113,c_tptpcol_1_1) = true,
inference(equational,[status(thm)],[c286,c19555,c19908]) ).
cnf(c20600,plain,
ifeq4(disjointwith(c_tptpcol_4_90113,X),true,disjointwith(c_tptpcol_5_90114,X),true) = true,
inference(equational,[status(thm)],[c40,c286,c18634]) ).
cnf(c20601,plain,
disjointwith(c_tptpcol_5_90114,c_tptpcol_1_1) = true,
inference(equational,[status(thm)],[c286,c19909,c20600]) ).
cnf(c21473,plain,
ifeq4(disjointwith(c_tptpcol_5_90114,X),true,disjointwith(c_tptpcol_6_92162,X),true) = true,
inference(equational,[status(thm)],[c45,c286,c18634]) ).
cnf(c21474,plain,
disjointwith(c_tptpcol_6_92162,c_tptpcol_1_1) = true,
inference(equational,[status(thm)],[c286,c20601,c21473]) ).
cnf(c22032,plain,
ifeq4(disjointwith(c_tptpcol_6_92162,X),true,disjointwith(c_tptpcol_7_93186,X),true) = true,
inference(equational,[status(thm)],[c232,c286,c18634]) ).
cnf(c22033,plain,
disjointwith(c_tptpcol_7_93186,c_tptpcol_1_1) = true,
inference(equational,[status(thm)],[c286,c21474,c22032]) ).
cnf(c22035,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_7_93186) = true,
inference(equational,[status(thm)],[c286,c5065,c22033]) ).
cnf(c30482,plain,
ifeq4(genls(X,c_tptpcol_1_1),true,disjointwith(X,c_tptpcol_7_93186),true) = true,
inference(equational,[status(thm)],[c286,c18634,c22035]) ).
cnf(c33784,axiom,
ifeq4(genls(X,Y),true,ifeq4(genls(Y,Z),true,genls(X,Z),true),true) = true,
file('theBenchmark.p',ax1_1112) ).
cnf(c33865,plain,
ifeq4(genls(c_tptpcol_9_18439,X),true,genls(c_tptpcol_10_18567,X),true) = true,
inference(equational,[status(thm)],[c263,c286,c33784]) ).
cnf(c33877,plain,
ifeq4(genls(c_tptpcol_9_93699,X),true,genls(c_tptpcol_10_93700,X),true) = true,
inference(equational,[status(thm)],[c134,c286,c33784]) ).
cnf(c33885,plain,
ifeq4(genls(c_tptpcol_10_18567,X),true,genls(c_tptpcol_11_18631,X),true) = true,
inference(equational,[status(thm)],[c184,c286,c33784]) ).
cnf(c33903,plain,
ifeq4(genls(c_tptpcol_10_93700,X),true,genls(c_tptpcol_11_93764,X),true) = true,
inference(equational,[status(thm)],[c130,c286,c33784]) ).
cnf(c33914,plain,
ifeq4(genls(c_tptpcol_11_18631,X),true,genls(c_tptpcol_12_18663,X),true) = true,
inference(equational,[status(thm)],[c215,c286,c33784]) ).
cnf(c33952,plain,
ifeq4(genls(c_tptpcol_12_18663,X),true,genls(c_tptpcol_13_18664,X),true) = true,
inference(equational,[status(thm)],[c169,c286,c33784]) ).
cnf(c33982,plain,
ifeq4(genls(c_tptpcol_12_93765,X),true,genls(c_tptpcol_13_93766,X),true) = true,
inference(equational,[status(thm)],[c225,c286,c33784]) ).
cnf(c33983,plain,
genls(c_tptpcol_13_93766,c_tptpcol_11_93764) = true,
inference(equational,[status(thm)],[c226,c286,c33982]) ).
cnf(c34029,plain,
ifeq4(genls(c_tptpcol_13_93766,X),true,genls(c_tptpcol_14_93774,X),true) = true,
inference(equational,[status(thm)],[c179,c286,c33784]) ).
cnf(c34031,plain,
genls(c_tptpcol_14_93774,c_tptpcol_11_93764) = true,
inference(equational,[status(thm)],[c286,c33983,c34029]) ).
cnf(c34077,plain,
ifeq4(genls(c_tptpcol_14_93774,X),true,genls(c_tptpcol_15_93775,X),true) = true,
inference(equational,[status(thm)],[c188,c286,c33784]) ).
cnf(c34080,plain,
genls(c_tptpcol_15_93775,c_tptpcol_11_93764) = true,
inference(equational,[status(thm)],[c286,c34031,c34077]) ).
cnf(c34155,plain,
ifeq4(genls(c_tptpcol_3_16386,X),true,genls(c_tptpcol_4_16387,X),true) = true,
inference(equational,[status(thm)],[c95,c286,c33784]) ).
cnf(c34156,plain,
genls(c_tptpcol_4_16387,c_tptpcol_2_2) = true,
inference(equational,[status(thm)],[c46,c286,c34155]) ).
cnf(c34193,plain,
ifeq4(genls(c_tptpcol_4_16387,X),true,genls(c_tptpcol_5_16388,X),true) = true,
inference(equational,[status(thm)],[c253,c286,c33784]) ).
cnf(c34195,plain,
genls(c_tptpcol_5_16388,c_tptpcol_2_2) = true,
inference(equational,[status(thm)],[c286,c34156,c34193]) ).
cnf(c34242,plain,
ifeq4(genls(c_tptpcol_5_16388,X),true,genls(c_tptpcol_6_18436,X),true) = true,
inference(equational,[status(thm)],[c117,c286,c33784]) ).
cnf(c34245,plain,
genls(c_tptpcol_6_18436,c_tptpcol_2_2) = true,
inference(equational,[status(thm)],[c286,c34195,c34242]) ).
cnf(c34299,plain,
ifeq4(genls(c_tptpcol_6_18436,X),true,genls(c_tptpcol_7_18437,X),true) = true,
inference(equational,[status(thm)],[c31,c286,c33784]) ).
cnf(c34303,plain,
genls(c_tptpcol_7_18437,c_tptpcol_2_2) = true,
inference(equational,[status(thm)],[c286,c34245,c34299]) ).
cnf(c34374,plain,
ifeq4(genls(c_tptpcol_7_18437,X),true,genls(c_tptpcol_8_18438,X),true) = true,
inference(equational,[status(thm)],[c121,c286,c33784]) ).
cnf(c34379,plain,
genls(c_tptpcol_8_18438,c_tptpcol_2_2) = true,
inference(equational,[status(thm)],[c286,c34303,c34374]) ).
cnf(c34510,plain,
ifeq4(genls(c_tptpcol_8_18438,X),true,genls(c_tptpcol_9_18439,X),true) = true,
inference(equational,[status(thm)],[c100,c286,c33784]) ).
cnf(c34528,plain,
genls(c_tptpcol_9_18439,c_tptpcol_2_2) = true,
inference(equational,[status(thm)],[c286,c34379,c34510]) ).
cnf(c34532,plain,
genls(c_tptpcol_10_18567,c_tptpcol_2_2) = true,
inference(equational,[status(thm)],[c286,c33865,c34528]) ).
cnf(c34538,plain,
genls(c_tptpcol_11_18631,c_tptpcol_2_2) = true,
inference(equational,[status(thm)],[c286,c33885,c34532]) ).
cnf(c34540,plain,
genls(c_tptpcol_12_18663,c_tptpcol_2_2) = true,
inference(equational,[status(thm)],[c286,c33914,c34538]) ).
cnf(c34544,plain,
genls(c_tptpcol_13_18664,c_tptpcol_2_2) = true,
inference(equational,[status(thm)],[c286,c33952,c34540]) ).
cnf(c34746,plain,
ifeq4(genls(c_tptpcol_8_93698,X),true,genls(c_tptpcol_9_93699,X),true) = true,
inference(equational,[status(thm)],[c129,c286,c33784]) ).
cnf(c34747,plain,
genls(c_tptpcol_9_93699,c_tptpcol_7_93186) = true,
inference(equational,[status(thm)],[c115,c286,c34746]) ).
cnf(c34748,plain,
genls(c_tptpcol_10_93700,c_tptpcol_7_93186) = true,
inference(equational,[status(thm)],[c286,c33877,c34747]) ).
cnf(c34751,plain,
genls(c_tptpcol_11_93764,c_tptpcol_7_93186) = true,
inference(equational,[status(thm)],[c286,c33903,c34748]) ).
cnf(c34910,plain,
ifeq4(genls(X,c_tptpcol_2_2),true,genls(X,c_tptpcol_1_1),true) = true,
inference(equational,[status(thm)],[c194,c286,c33784]) ).
cnf(c35000,plain,
genls(c_tptpcol_13_18664,c_tptpcol_1_1) = true,
inference(equational,[status(thm)],[c286,c34544,c34910]) ).
cnf(c36233,plain,
disjointwith(c_tptpcol_13_18664,c_tptpcol_7_93186) = true,
inference(equational,[status(thm)],[c286,c30482,c35000]) ).
cnf(c36378,plain,
disjointwith(c_tptpcol_7_93186,c_tptpcol_13_18664) = true,
inference(equational,[status(thm)],[c286,c5065,c36233]) ).
cnf(c38160,plain,
ifeq4(disjointwith(c_tptpcol_11_93764,X),true,disjointwith(c_tptpcol_15_93775,X),true) = true,
inference(equational,[status(thm)],[c286,c18634,c34080]) ).
cnf(c38559,plain,
ifeq4(disjointwith(c_tptpcol_7_93186,X),true,disjointwith(c_tptpcol_11_93764,X),true) = true,
inference(equational,[status(thm)],[c286,c18634,c34751]) ).
cnf(c38560,plain,
disjointwith(c_tptpcol_11_93764,c_tptpcol_13_18664) = true,
inference(equational,[status(thm)],[c286,c36378,c38559]) ).
cnf(c38676,plain,
disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) = true,
inference(equational,[status(thm)],[c286,c38160,c38560]) ).
cnf(c38677,plain,
b = a,
inference(equational,[status(thm)],[c284,c538,c38676]) ).
cnf(g1,plain,
a = b,
inference(equational,[status(thm)],[c38677]) ).
cnf(g2,plain,
$false,
inference(resolution,[status(thm)],[g0,g1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : CSR039-10 : TPTP v9.0.0. Released v7.3.0.
% 0.03/0.13 % Command : run_Leo-III %s %d THM
% 0.12/0.34 % Computer : n005.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Jul 14 05:17:04 EDT 2025
% 0.12/0.34 % CPUTime :
% 77.11/77.18 % SZS status Unsatisfiable
% 77.11/77.18 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------