%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR039+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n015.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 : Fri Sep 25 01:05:22 PM UTC 2026
% Result : Theorem 98.19s 12.98s
% Output : Proof 98.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 41
% Syntax : Number of formulae : 202 ( 158 unt; 0 def)
% Number of atoms : 262 ( 63 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 144 ( 84 ~; 42 |; 12 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 1 prp; 0-2 aty)
% Number of functors : 36 ( 36 usr; 32 con; 0-4 aty)
% Number of variables : 99 ( 0 sgn 66 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1112,axiom,
! [ARG1,OLD,NEW] :
( ( genls(OLD,NEW)
& genls(ARG1,OLD) )
=> genls(ARG1,NEW) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_1113) ).
fof(f1112_nnf,plain,
! [ARG1,OLD,NEW] :
( genls(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ genls(ARG1,OLD) ),
inference(nnf_transformation,[status(thm)],[f1112]) ).
fof(f1112_sk,plain,
! [ARG1,OLD,NEW] :
( genls(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ genls(ARG1,OLD) ),
inference(skolemisation,[status(esa)],[f1112_nnf]) ).
cnf(c1112,plain,
( genls(X0,X2)
| ~ genls(X1,X2)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1112_sk]) ).
cnf(hi1103,axiom,
ifeq(genls(X0,X1),true,ifeq(genls(X1,X2),true,genls(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c1112]) ).
fof(f40,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_41) ).
fof(f40_nnf,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(nnf_transformation,[status(thm)],[f40]) ).
cnf(c40,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(cnf_transformation,[status(esa)],[f40_nnf]) ).
cnf(hi39,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537) = true,
inference(equality_encoding,[status(esa)],[c40]) ).
fof(f347,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_348) ).
fof(f347_nnf,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(nnf_transformation,[status(thm)],[f347]) ).
cnf(c347,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[status(esa)],[f347_nnf]) ).
cnf(hi343,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536) = true,
inference(equality_encoding,[status(esa)],[c347]) ).
cnf(h1743,plain,
genls(c_tptpcol_3_81921,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi39,hi343]) ).
fof(f375,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_376) ).
fof(f375_nnf,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(nnf_transformation,[status(thm)],[f375]) ).
cnf(c375,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(cnf_transformation,[status(esa)],[f375_nnf]) ).
cnf(hi370,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921) = true,
inference(equality_encoding,[status(esa)],[c375]) ).
cnf(h4159,plain,
genls(c_tptpcol_4_90113,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi370,h1743]) ).
fof(f13,axiom,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_14) ).
fof(f13_nnf,plain,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c13,plain,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(hi12,axiom,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
fof(f416,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_417) ).
fof(f416_nnf,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(nnf_transformation,[status(thm)],[f416]) ).
cnf(c416,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(cnf_transformation,[status(esa)],[f416_nnf]) ).
cnf(hi411,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114) = true,
inference(equality_encoding,[status(esa)],[c416]) ).
cnf(h1961,plain,
genls(c_tptpcol_7_93186,c_tptpcol_5_90114) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi12,hi411]) ).
fof(f475,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_476) ).
fof(f475_nnf,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(nnf_transformation,[status(thm)],[f475]) ).
cnf(c475,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(cnf_transformation,[status(esa)],[f475_nnf]) ).
cnf(hi470,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113) = true,
inference(equality_encoding,[status(esa)],[c475]) ).
cnf(h4507,plain,
genls(c_tptpcol_7_93186,c_tptpcol_4_90113) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h1961,hi470]) ).
cnf(h5974,plain,
genls(c_tptpcol_7_93186,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h4507,h4159]) ).
fof(f369,axiom,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_370) ).
fof(f369_nnf,plain,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
inference(nnf_transformation,[status(thm)],[f369]) ).
cnf(c369,plain,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
inference(cnf_transformation,[status(esa)],[f369_nnf]) ).
cnf(hi364,axiom,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698) = true,
inference(equality_encoding,[status(esa)],[c369]) ).
fof(f344,axiom,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_345) ).
fof(f344_nnf,plain,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
inference(nnf_transformation,[status(thm)],[f344]) ).
cnf(c344,plain,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
inference(cnf_transformation,[status(esa)],[f344_nnf]) ).
cnf(hi340,axiom,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186) = true,
inference(equality_encoding,[status(esa)],[c344]) ).
cnf(h1817,plain,
genls(c_tptpcol_9_93699,c_tptpcol_7_93186) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi364,hi340]) ).
fof(f371,axiom,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_372) ).
fof(f371_nnf,plain,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
inference(nnf_transformation,[status(thm)],[f371]) ).
cnf(c371,plain,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
inference(cnf_transformation,[status(esa)],[f371_nnf]) ).
cnf(hi366,axiom,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700) = true,
inference(equality_encoding,[status(esa)],[c371]) ).
fof(f378,axiom,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_379) ).
fof(f378_nnf,plain,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
inference(nnf_transformation,[status(thm)],[f378]) ).
cnf(c378,plain,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
inference(cnf_transformation,[status(esa)],[f378_nnf]) ).
cnf(hi373,axiom,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699) = true,
inference(equality_encoding,[status(esa)],[c378]) ).
cnf(h1837,plain,
genls(c_tptpcol_11_93764,c_tptpcol_9_93699) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi366,hi373]) ).
cnf(h4326,plain,
genls(c_tptpcol_11_93764,c_tptpcol_7_93186) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h1837,h1817]) ).
fof(f77,axiom,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_78) ).
fof(f77_nnf,plain,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
inference(nnf_transformation,[status(thm)],[f77]) ).
cnf(c77,plain,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
inference(cnf_transformation,[status(esa)],[f77_nnf]) ).
cnf(hi76,axiom,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765) = true,
inference(equality_encoding,[status(esa)],[c77]) ).
fof(f71,axiom,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_72) ).
fof(f71_nnf,plain,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
inference(nnf_transformation,[status(thm)],[f71]) ).
cnf(c71,plain,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
inference(cnf_transformation,[status(esa)],[f71_nnf]) ).
cnf(hi70,axiom,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764) = true,
inference(equality_encoding,[status(esa)],[c71]) ).
cnf(h585,plain,
genls(c_tptpcol_13_93766,c_tptpcol_11_93764) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi76,hi70]) ).
fof(f181,axiom,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_182) ).
fof(f181_nnf,plain,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
inference(nnf_transformation,[status(thm)],[f181]) ).
cnf(c181,plain,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
inference(cnf_transformation,[status(esa)],[f181_nnf]) ).
cnf(hi178,axiom,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774) = true,
inference(equality_encoding,[status(esa)],[c181]) ).
fof(f190,axiom,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_191) ).
fof(f190_nnf,plain,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
inference(nnf_transformation,[status(thm)],[f190]) ).
cnf(c190,plain,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
inference(cnf_transformation,[status(esa)],[f190_nnf]) ).
cnf(hi187,axiom,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766) = true,
inference(equality_encoding,[status(esa)],[c190]) ).
cnf(h1139,plain,
genls(c_tptpcol_15_93775,c_tptpcol_13_93766) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi178,hi187]) ).
cnf(h3389,plain,
genls(c_tptpcol_15_93775,c_tptpcol_11_93764) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h1139,h585]) ).
cnf(h5705,plain,
genls(c_tptpcol_15_93775,c_tptpcol_7_93186) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h3389,h4326]) ).
cnf(h9686,plain,
genls(c_tptpcol_15_93775,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h5705,h5974]) ).
fof(f254,axiom,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_255) ).
fof(f254_nnf,plain,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
inference(nnf_transformation,[status(thm)],[f254]) ).
cnf(c254,plain,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
inference(cnf_transformation,[status(esa)],[f254_nnf]) ).
cnf(hi251,axiom,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438) = true,
inference(equality_encoding,[status(esa)],[c254]) ).
fof(f352,axiom,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_353) ).
fof(f352_nnf,plain,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
inference(nnf_transformation,[status(thm)],[f352]) ).
cnf(c352,plain,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
inference(cnf_transformation,[status(esa)],[f352_nnf]) ).
cnf(hi348,axiom,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437) = true,
inference(equality_encoding,[status(esa)],[c352]) ).
cnf(h1770,plain,
genls(c_tptpcol_9_18439,c_tptpcol_7_18437) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi251,hi348]) ).
fof(f482,axiom,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_483) ).
fof(f482_nnf,plain,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
inference(nnf_transformation,[status(thm)],[f482]) ).
cnf(c482,plain,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
inference(cnf_transformation,[status(esa)],[f482_nnf]) ).
cnf(hi477,axiom,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436) = true,
inference(equality_encoding,[status(esa)],[c482]) ).
cnf(h4182,plain,
genls(c_tptpcol_9_18439,c_tptpcol_6_18436) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h1770,hi477]) ).
fof(f174,axiom,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_175) ).
fof(f174_nnf,plain,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
inference(nnf_transformation,[status(thm)],[f174]) ).
cnf(c174,plain,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
inference(cnf_transformation,[status(esa)],[f174_nnf]) ).
cnf(hi171,axiom,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567) = true,
inference(equality_encoding,[status(esa)],[c174]) ).
fof(f42,axiom,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_43) ).
fof(f42_nnf,plain,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
inference(nnf_transformation,[status(thm)],[f42]) ).
cnf(c42,plain,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
inference(cnf_transformation,[status(esa)],[f42_nnf]) ).
cnf(hi41,axiom,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439) = true,
inference(equality_encoding,[status(esa)],[c42]) ).
cnf(h1091,plain,
genls(c_tptpcol_11_18631,c_tptpcol_9_18439) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi171,hi41]) ).
fof(f207,axiom,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_208) ).
fof(f207_nnf,plain,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
inference(nnf_transformation,[status(thm)],[f207]) ).
cnf(c207,plain,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
inference(cnf_transformation,[status(esa)],[f207_nnf]) ).
cnf(hi204,axiom,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663) = true,
inference(equality_encoding,[status(esa)],[c207]) ).
fof(f108,axiom,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_109) ).
fof(f108_nnf,plain,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
inference(nnf_transformation,[status(thm)],[f108]) ).
cnf(c108,plain,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
inference(cnf_transformation,[status(esa)],[f108_nnf]) ).
cnf(hi107,axiom,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631) = true,
inference(equality_encoding,[status(esa)],[c108]) ).
cnf(h1177,plain,
genls(c_tptpcol_13_18664,c_tptpcol_11_18631) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi204,hi107]) ).
cnf(h3439,plain,
genls(c_tptpcol_13_18664,c_tptpcol_9_18439) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h1177,h1091]) ).
cnf(h5594,plain,
genls(c_tptpcol_13_18664,c_tptpcol_6_18436) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h3439,h4182]) ).
fof(f284,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_285) ).
fof(f284_nnf,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(nnf_transformation,[status(thm)],[f284]) ).
cnf(c284,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(cnf_transformation,[status(esa)],[f284_nnf]) ).
cnf(hi281,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386) = true,
inference(equality_encoding,[status(esa)],[c284]) ).
fof(f384,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_385) ).
fof(f384_nnf,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(nnf_transformation,[status(thm)],[f384]) ).
cnf(c384,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[status(esa)],[f384_nnf]) ).
cnf(hi379,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2) = true,
inference(equality_encoding,[status(esa)],[c384]) ).
cnf(h1863,plain,
genls(c_tptpcol_4_16387,c_tptpcol_2_2) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi281,hi379]) ).
fof(f350,axiom,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_351) ).
fof(f350_nnf,plain,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
inference(nnf_transformation,[status(thm)],[f350]) ).
cnf(c350,plain,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
inference(cnf_transformation,[status(esa)],[f350_nnf]) ).
cnf(hi346,axiom,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388) = true,
inference(equality_encoding,[status(esa)],[c350]) ).
fof(f22,axiom,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_23) ).
fof(f22_nnf,plain,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
inference(nnf_transformation,[status(thm)],[f22]) ).
cnf(c22,plain,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
inference(cnf_transformation,[status(esa)],[f22_nnf]) ).
cnf(hi21,axiom,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387) = true,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(h1765,plain,
genls(c_tptpcol_6_18436,c_tptpcol_4_16387) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi346,hi21]) ).
cnf(h4343,plain,
genls(c_tptpcol_6_18436,c_tptpcol_2_2) = true,
inference(hyper_resolution,[status(thm)],[hi1103,h1765,h1863]) ).
fof(f1121,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_1122) ).
fof(f1121_nnf,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(nnf_transformation,[status(thm)],[f1121]) ).
fof(f1121_sk,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(skolemisation,[status(esa)],[f1121_nnf]) ).
cnf(c1121,plain,
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1121_sk]) ).
cnf(hi1112,axiom,
ifeq(disjointwith(X0,X1),true,ifeq(genls(X2,X0),true,disjointwith(X2,X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c1121]) ).
fof(f151,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_152) ).
fof(f151_nnf,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(nnf_transformation,[status(thm)],[f151]) ).
cnf(c151,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[status(esa)],[f151_nnf]) ).
cnf(hi150,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) = true,
inference(equality_encoding,[status(esa)],[c151]) ).
fof(f144,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_145) ).
fof(f144_nnf,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(nnf_transformation,[status(thm)],[f144]) ).
cnf(c144,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[status(esa)],[f144_nnf]) ).
cnf(hi143,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1) = true,
inference(equality_encoding,[status(esa)],[c144]) ).
cnf(h999,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi1112,hi150,hi143]) ).
fof(f1119,axiom,
! [X,Y] :
( disjointwith(X,Y)
=> disjointwith(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_1120) ).
fof(f1119_nnf,plain,
! [X,Y] :
( disjointwith(Y,X)
| ~ disjointwith(X,Y) ),
inference(nnf_transformation,[status(thm)],[f1119]) ).
fof(f1119_sk,plain,
! [X,Y] :
( disjointwith(Y,X)
| ~ disjointwith(X,Y) ),
inference(skolemisation,[status(esa)],[f1119_nnf]) ).
cnf(c1119,plain,
( disjointwith(X1,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1119_sk]) ).
cnf(hi1110,axiom,
ifeq(disjointwith(X0,X1),true,disjointwith(X1,X0),true) = true,
inference(equality_encoding,[status(esa)],[c1119]) ).
cnf(h3202,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_2_2) = true,
inference(hyper_resolution,[status(thm)],[hi1110,h999]) ).
fof(f1120,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_1121) ).
fof(f1120_nnf,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(nnf_transformation,[status(thm)],[f1120]) ).
fof(f1120_sk,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(skolemisation,[status(esa)],[f1120_nnf]) ).
cnf(c1120,plain,
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1120_sk]) ).
cnf(hi1111,axiom,
ifeq(disjointwith(X0,X1),true,ifeq(genls(X2,X1),true,disjointwith(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c1120]) ).
cnf(h5748,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_6_18436) = true,
inference(hyper_resolution,[status(thm)],[hi1111,h3202,h4343]) ).
cnf(h8660,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_13_18664) = true,
inference(hyper_resolution,[status(thm)],[hi1111,h5748,h5594]) ).
cnf(h18120,plain,
disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) = true,
inference(hyper_resolution,[status(thm)],[hi1112,h8660,h9686]) ).
fof(f1131,conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))
=> disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query89) ).
fof(f1131_neg,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))
=> disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ),
inference(negated_conjecture,[status(cth)],[f1131]) ).
fof(f1131_nnf,plain,
( ~ disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664)
& mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7)) ),
inference(nnf_transformation,[status(thm)],[f1131_neg]) ).
fof(f1131_sk,plain,
( ~ disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664)
& mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7)) ),
inference(skolemisation,[status(esa)],[f1131_nnf]) ).
cnf(c1132,plain,
~ disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),
inference(cnf_transformation,[status(esa)],[f1131_sk]) ).
cnf(hi1132,negated_conjecture,
ifeq(disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c1132]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi1132,h18120]) ).
cnf(t780,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f2,axiom,
! [OBJ] :
~ ( partiallytangible(OBJ)
& intangible(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_3) ).
fof(f2_nnf,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ intangible(OBJ) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ intangible(OBJ) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( ~ partiallytangible(X0)
| ~ intangible(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
fof(f152,axiom,
! [OBJ] :
~ ( tptpcol_1_65536(OBJ)
& tptpcol_1_1(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_153) ).
fof(f152_nnf,plain,
! [OBJ] :
( ~ tptpcol_1_65536(OBJ)
| ~ tptpcol_1_1(OBJ) ),
inference(nnf_transformation,[status(thm)],[f152]) ).
fof(f152_sk,plain,
! [OBJ] :
( ~ tptpcol_1_65536(OBJ)
| ~ tptpcol_1_1(OBJ) ),
inference(skolemisation,[status(esa)],[f152_nnf]) ).
cnf(c152,plain,
( ~ tptpcol_1_65536(X0)
| ~ tptpcol_1_1(X0) ),
inference(cnf_transformation,[status(esa)],[f152_sk]) ).
fof(f166,axiom,
! [OBJ] :
~ ( setorcollection(OBJ)
& individual(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_167) ).
fof(f166_nnf,plain,
! [OBJ] :
( ~ setorcollection(OBJ)
| ~ individual(OBJ) ),
inference(nnf_transformation,[status(thm)],[f166]) ).
fof(f166_sk,plain,
! [OBJ] :
( ~ setorcollection(OBJ)
| ~ individual(OBJ) ),
inference(skolemisation,[status(esa)],[f166_nnf]) ).
cnf(c166,plain,
( ~ setorcollection(X0)
| ~ individual(X0) ),
inference(cnf_transformation,[status(esa)],[f166_sk]) ).
fof(f288,axiom,
! [OBJ] :
~ ( individual(OBJ)
& collection(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_289) ).
fof(f288_nnf,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(nnf_transformation,[status(thm)],[f288]) ).
fof(f288_sk,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(skolemisation,[status(esa)],[f288_nnf]) ).
cnf(c288,plain,
( ~ individual(X0)
| ~ collection(X0) ),
inference(cnf_transformation,[status(esa)],[f288_sk]) ).
fof(f362,axiom,
! [OBJ,COL1,COL2] :
~ ( disjointwith(COL1,COL2)
& isa(OBJ,COL2)
& isa(OBJ,COL1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_363) ).
fof(f362_nnf,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(nnf_transformation,[status(thm)],[f362]) ).
fof(f362_sk,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(skolemisation,[status(esa)],[f362_nnf]) ).
cnf(c362,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X0,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f362_sk]) ).
fof(f487,axiom,
! [OBJ] :
~ ( tptpcol_3_114688(OBJ)
& tptpcol_3_98305(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_488) ).
fof(f487_nnf,plain,
! [OBJ] :
( ~ tptpcol_3_114688(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(nnf_transformation,[status(thm)],[f487]) ).
fof(f487_sk,plain,
! [OBJ] :
( ~ tptpcol_3_114688(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(skolemisation,[status(esa)],[f487_nnf]) ).
cnf(c487,plain,
( ~ tptpcol_3_114688(X0)
| ~ tptpcol_3_98305(X0) ),
inference(cnf_transformation,[status(esa)],[f487_sk]) ).
fof(f520,axiom,
! [X] : ~ affiliatedwith(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_521) ).
fof(f520_nnf,plain,
! [X] : ~ affiliatedwith(X,X),
inference(nnf_transformation,[status(thm)],[f520]) ).
fof(f520_sk,plain,
! [X] : ~ affiliatedwith(X,X),
inference(skolemisation,[status(esa)],[f520_nnf]) ).
cnf(c520,plain,
~ affiliatedwith(X0,X0),
inference(cnf_transformation,[status(esa)],[f520_sk]) ).
fof(f697,axiom,
! [X] : ~ objectfoundinlocation(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_698) ).
fof(f697_nnf,plain,
! [X] : ~ objectfoundinlocation(X,X),
inference(nnf_transformation,[status(thm)],[f697]) ).
fof(f697_sk,plain,
! [X] : ~ objectfoundinlocation(X,X),
inference(skolemisation,[status(esa)],[f697_nnf]) ).
cnf(c697,plain,
~ objectfoundinlocation(X0,X0),
inference(cnf_transformation,[status(esa)],[f697_sk]) ).
fof(f900,axiom,
! [X] : ~ borderson(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1_901) ).
fof(f900_nnf,plain,
! [X] : ~ borderson(X,X),
inference(nnf_transformation,[status(thm)],[f900]) ).
fof(f900_sk,plain,
! [X] : ~ borderson(X,X),
inference(skolemisation,[status(esa)],[f900_nnf]) ).
cnf(c900,plain,
~ borderson(X0,X0),
inference(cnf_transformation,[status(esa)],[f900_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2,c152,c166,c288,c362,c487,c520,c697,c900,c1132]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t780]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR039+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n015.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 08:26:41 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 98.19/12.98 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 98.19/12.98 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------