%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR036+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n009.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:20 PM UTC 2026
% Result : Theorem 8.75s 1.67s
% Output : Proof 8.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 36
% Syntax : Number of formulae : 183 ( 159 unt; 0 def)
% Number of atoms : 223 ( 67 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 81 ( 41 ~; 27 |; 8 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 34 con; 0-4 aty)
% Number of variables : 61 ( 0 sgn 39 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f155,axiom,
! [ARG1,OLD,NEW] :
( ( genls(OLD,NEW)
& genls(ARG1,OLD) )
=> genls(ARG1,NEW) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just156) ).
fof(f155_nnf,plain,
! [ARG1,OLD,NEW] :
( genls(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ genls(ARG1,OLD) ),
inference(nnf_transformation,[status(thm)],[f155]) ).
fof(f155_sk,plain,
! [ARG1,OLD,NEW] :
( genls(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ genls(ARG1,OLD) ),
inference(skolemisation,[status(esa)],[f155_nnf]) ).
cnf(c155,plain,
( genls(X0,X2)
| ~ genls(X1,X2)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f155_sk]) ).
cnf(hi153,axiom,
ifeq(genls(X0,X1),true,ifeq(genls(X1,X2),true,genls(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c155]) ).
fof(f35,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just36) ).
fof(f35_nnf,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(nnf_transformation,[status(thm)],[f35]) ).
cnf(c35,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(cnf_transformation,[status(esa)],[f35_nnf]) ).
cnf(hi35,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537) = true,
inference(equality_encoding,[status(esa)],[c35]) ).
fof(f33,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just34) ).
fof(f33_nnf,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(nnf_transformation,[status(thm)],[f33]) ).
cnf(c33,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[status(esa)],[f33_nnf]) ).
cnf(hi33,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536) = true,
inference(equality_encoding,[status(esa)],[c33]) ).
cnf(h42,plain,
genls(c_tptpcol_3_65538,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi153,hi35,hi33]) ).
fof(f39,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just40) ).
fof(f39_nnf,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(nnf_transformation,[status(thm)],[f39]) ).
cnf(c39,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(cnf_transformation,[status(esa)],[f39_nnf]) ).
cnf(hi39,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539) = true,
inference(equality_encoding,[status(esa)],[c39]) ).
fof(f37,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just38) ).
fof(f37_nnf,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(nnf_transformation,[status(thm)],[f37]) ).
cnf(c37,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(cnf_transformation,[status(esa)],[f37_nnf]) ).
cnf(hi37,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538) = true,
inference(equality_encoding,[status(esa)],[c37]) ).
cnf(h47,plain,
genls(c_tptpcol_5_69635,c_tptpcol_3_65538) = true,
inference(hyper_resolution,[status(thm)],[hi153,hi39,hi37]) ).
cnf(h133,plain,
genls(c_tptpcol_5_69635,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi153,h47,h42]) ).
fof(f43,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just44) ).
fof(f43_nnf,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(nnf_transformation,[status(thm)],[f43]) ).
cnf(c43,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(cnf_transformation,[status(esa)],[f43_nnf]) ).
cnf(hi43,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683) = true,
inference(equality_encoding,[status(esa)],[c43]) ).
fof(f41,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just42) ).
fof(f41_nnf,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(nnf_transformation,[status(thm)],[f41]) ).
cnf(c41,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(cnf_transformation,[status(esa)],[f41_nnf]) ).
cnf(hi41,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635) = true,
inference(equality_encoding,[status(esa)],[c41]) ).
cnf(h51,plain,
genls(c_tptpcol_7_72707,c_tptpcol_5_69635) = true,
inference(hyper_resolution,[status(thm)],[hi153,hi43,hi41]) ).
fof(f47,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just48) ).
fof(f47_nnf,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(nnf_transformation,[status(thm)],[f47]) ).
cnf(c47,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(cnf_transformation,[status(esa)],[f47_nnf]) ).
cnf(hi47,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708) = true,
inference(equality_encoding,[status(esa)],[c47]) ).
fof(f45,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just46) ).
fof(f45_nnf,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(nnf_transformation,[status(thm)],[f45]) ).
cnf(c45,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(cnf_transformation,[status(esa)],[f45_nnf]) ).
cnf(hi45,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707) = true,
inference(equality_encoding,[status(esa)],[c45]) ).
cnf(h56,plain,
genls(c_tptpcol_9_72709,c_tptpcol_7_72707) = true,
inference(hyper_resolution,[status(thm)],[hi153,hi47,hi45]) ).
cnf(h146,plain,
genls(c_tptpcol_9_72709,c_tptpcol_5_69635) = true,
inference(hyper_resolution,[status(thm)],[hi153,h56,h51]) ).
cnf(h256,plain,
genls(c_tptpcol_9_72709,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi153,h146,h133]) ).
fof(f51,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just52) ).
fof(f51_nnf,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(nnf_transformation,[status(thm)],[f51]) ).
cnf(c51,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(cnf_transformation,[status(esa)],[f51_nnf]) ).
cnf(hi51,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710) = true,
inference(equality_encoding,[status(esa)],[c51]) ).
fof(f49,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just50) ).
fof(f49_nnf,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(nnf_transformation,[status(thm)],[f49]) ).
cnf(c49,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(cnf_transformation,[status(esa)],[f49_nnf]) ).
cnf(hi49,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709) = true,
inference(equality_encoding,[status(esa)],[c49]) ).
cnf(h61,plain,
genls(c_tptpcol_11_72774,c_tptpcol_9_72709) = true,
inference(hyper_resolution,[status(thm)],[hi153,hi51,hi49]) ).
fof(f55,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just56) ).
fof(f55_nnf,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(nnf_transformation,[status(thm)],[f55]) ).
cnf(c55,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(cnf_transformation,[status(esa)],[f55_nnf]) ).
cnf(hi55,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775) = true,
inference(equality_encoding,[status(esa)],[c55]) ).
fof(f53,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just54) ).
fof(f53_nnf,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(nnf_transformation,[status(thm)],[f53]) ).
cnf(c53,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(cnf_transformation,[status(esa)],[f53_nnf]) ).
cnf(hi53,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774) = true,
inference(equality_encoding,[status(esa)],[c53]) ).
cnf(h65,plain,
genls(c_tptpcol_13_72791,c_tptpcol_11_72774) = true,
inference(hyper_resolution,[status(thm)],[hi153,hi55,hi53]) ).
cnf(h157,plain,
genls(c_tptpcol_13_72791,c_tptpcol_9_72709) = true,
inference(hyper_resolution,[status(thm)],[hi153,h65,h61]) ).
fof(f59,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just60) ).
fof(f59_nnf,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(nnf_transformation,[status(thm)],[f59]) ).
cnf(c59,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(cnf_transformation,[status(esa)],[f59_nnf]) ).
cnf(hi59,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792) = true,
inference(equality_encoding,[status(esa)],[c59]) ).
fof(f57,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just58) ).
fof(f57_nnf,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(nnf_transformation,[status(thm)],[f57]) ).
cnf(c57,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(cnf_transformation,[status(esa)],[f57_nnf]) ).
cnf(hi57,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791) = true,
inference(equality_encoding,[status(esa)],[c57]) ).
cnf(h70,plain,
genls(c_tptpcol_15_72793,c_tptpcol_13_72791) = true,
inference(hyper_resolution,[status(thm)],[hi153,hi59,hi57]) ).
fof(f61,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just62) ).
fof(f61_nnf,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(nnf_transformation,[status(thm)],[f61]) ).
cnf(c61,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(cnf_transformation,[status(esa)],[f61_nnf]) ).
cnf(hi61,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793) = true,
inference(equality_encoding,[status(esa)],[c61]) ).
cnf(h162,plain,
genls(c_tptpcol_16_72795,c_tptpcol_13_72791) = true,
inference(hyper_resolution,[status(thm)],[hi153,hi61,h70]) ).
cnf(h276,plain,
genls(c_tptpcol_16_72795,c_tptpcol_9_72709) = true,
inference(hyper_resolution,[status(thm)],[hi153,h162,h157]) ).
cnf(h478,plain,
genls(c_tptpcol_16_72795,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi153,h276,h256]) ).
fof(f19,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just20) ).
fof(f19_nnf,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(nnf_transformation,[status(thm)],[f19]) ).
cnf(c19,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(cnf_transformation,[status(esa)],[f19_nnf]) ).
cnf(hi19,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020) = true,
inference(equality_encoding,[status(esa)],[c19]) ).
fof(f17,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just18) ).
fof(f17_nnf,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(nnf_transformation,[status(thm)],[f17]) ).
cnf(c17,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(cnf_transformation,[status(esa)],[f17_nnf]) ).
cnf(hi17,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508) = true,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(h23,plain,
genls(c_tptpcol_9_22021,c_tptpcol_7_21508) = true,
inference(hyper_resolution,[status(thm)],[hi153,hi19,hi17]) ).
fof(f23,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just24) ).
fof(f23_nnf,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(nnf_transformation,[status(thm)],[f23]) ).
cnf(c23,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(cnf_transformation,[status(esa)],[f23_nnf]) ).
cnf(hi23,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022) = true,
inference(equality_encoding,[status(esa)],[c23]) ).
fof(f21,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just22) ).
fof(f21_nnf,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(nnf_transformation,[status(thm)],[f21]) ).
cnf(c21,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(cnf_transformation,[status(esa)],[f21_nnf]) ).
cnf(hi21,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(h28,plain,
genls(c_tptpcol_11_22023,c_tptpcol_9_22021) = true,
inference(hyper_resolution,[status(thm)],[hi153,hi23,hi21]) ).
cnf(h113,plain,
genls(c_tptpcol_11_22023,c_tptpcol_7_21508) = true,
inference(hyper_resolution,[status(thm)],[hi153,h28,h23]) ).
fof(f27,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just28) ).
fof(f27_nnf,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(nnf_transformation,[status(thm)],[f27]) ).
cnf(c27,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(cnf_transformation,[status(esa)],[f27_nnf]) ).
cnf(hi27,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055) = true,
inference(equality_encoding,[status(esa)],[c27]) ).
fof(f25,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just26) ).
fof(f25_nnf,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(nnf_transformation,[status(thm)],[f25]) ).
cnf(c25,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(cnf_transformation,[status(esa)],[f25_nnf]) ).
cnf(hi25,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023) = true,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(h33,plain,
genls(c_tptpcol_13_22071,c_tptpcol_11_22023) = true,
inference(hyper_resolution,[status(thm)],[hi153,hi27,hi25]) ).
fof(f31,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just32) ).
fof(f31_nnf,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(nnf_transformation,[status(thm)],[f31]) ).
cnf(c31,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(cnf_transformation,[status(esa)],[f31_nnf]) ).
cnf(hi31,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072) = true,
inference(equality_encoding,[status(esa)],[c31]) ).
fof(f29,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just30) ).
fof(f29_nnf,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(nnf_transformation,[status(thm)],[f29]) ).
cnf(c29,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(cnf_transformation,[status(esa)],[f29_nnf]) ).
cnf(hi29,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071) = true,
inference(equality_encoding,[status(esa)],[c29]) ).
cnf(h37,plain,
genls(c_tptpcol_15_22076,c_tptpcol_13_22071) = true,
inference(hyper_resolution,[status(thm)],[hi153,hi31,hi29]) ).
cnf(h123,plain,
genls(c_tptpcol_15_22076,c_tptpcol_11_22023) = true,
inference(hyper_resolution,[status(thm)],[hi153,h37,h33]) ).
cnf(h229,plain,
genls(c_tptpcol_15_22076,c_tptpcol_7_21508) = true,
inference(hyper_resolution,[status(thm)],[hi153,h123,h113]) ).
fof(f11,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just12) ).
fof(f11_nnf,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(hi11,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
fof(f9,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just10) ).
fof(f9_nnf,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(hi9,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(h15,plain,
genls(c_tptpcol_5_20483,c_tptpcol_3_16386) = true,
inference(hyper_resolution,[status(thm)],[hi153,hi11,hi9]) ).
fof(f15,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just16) ).
fof(f15_nnf,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(nnf_transformation,[status(thm)],[f15]) ).
cnf(c15,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(cnf_transformation,[status(esa)],[f15_nnf]) ).
cnf(hi15,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484) = true,
inference(equality_encoding,[status(esa)],[c15]) ).
fof(f13,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just14) ).
fof(f13_nnf,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c13,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(hi13,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(h19,plain,
genls(c_tptpcol_7_21508,c_tptpcol_5_20483) = true,
inference(hyper_resolution,[status(thm)],[hi153,hi15,hi13]) ).
cnf(h100,plain,
genls(c_tptpcol_7_21508,c_tptpcol_3_16386) = true,
inference(hyper_resolution,[status(thm)],[hi153,h19,h15]) ).
fof(f7,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just8) ).
fof(f7_nnf,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c7,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(hi7,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
fof(f5,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just6) ).
fof(f5_nnf,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(hi5,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(h11,plain,
genls(c_tptpcol_3_16386,c_tptpcol_1_1) = true,
inference(hyper_resolution,[status(thm)],[hi153,hi7,hi5]) ).
fof(f84,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just85) ).
fof(f84_nnf,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(nnf_transformation,[status(thm)],[f84]) ).
fof(f84_sk,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(skolemisation,[status(esa)],[f84_nnf]) ).
cnf(c84,plain,
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f84_sk]) ).
cnf(hi82,axiom,
ifeq(disjointwith(X0,X1),true,ifeq(genls(X2,X0),true,disjointwith(X2,X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c84]) ).
fof(f63,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just64) ).
fof(f63_nnf,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(nnf_transformation,[status(thm)],[f63]) ).
cnf(c63,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[status(esa)],[f63_nnf]) ).
cnf(hi63,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536) = true,
inference(equality_encoding,[status(esa)],[c63]) ).
cnf(h92,plain,
disjointwith(c_tptpcol_3_16386,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi82,hi63,h11]) ).
cnf(h204,plain,
disjointwith(c_tptpcol_7_21508,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi82,h92,h100]) ).
cnf(h372,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_1_65536) = true,
inference(hyper_resolution,[status(thm)],[hi82,h204,h229]) ).
fof(f83,axiom,
! [ARG1,OLD,NEW] :
( ( genls(NEW,OLD)
& disjointwith(ARG1,OLD) )
=> disjointwith(ARG1,NEW) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just84) ).
fof(f83_nnf,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(nnf_transformation,[status(thm)],[f83]) ).
fof(f83_sk,plain,
! [ARG1,OLD,NEW] :
( disjointwith(ARG1,NEW)
| ~ genls(NEW,OLD)
| ~ disjointwith(ARG1,OLD) ),
inference(skolemisation,[status(esa)],[f83_nnf]) ).
cnf(c83,plain,
( disjointwith(X0,X2)
| ~ genls(X2,X1)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f83_sk]) ).
cnf(hi81,axiom,
ifeq(disjointwith(X0,X1),true,ifeq(genls(X2,X1),true,disjointwith(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c83]) ).
cnf(h766,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) = true,
inference(hyper_resolution,[status(thm)],[hi81,h372,h478]) ).
fof(f173,conjecture,
( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query36) ).
fof(f173_neg,negated_conjecture,
~ ( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(negated_conjecture,[status(cth)],[f173]) ).
fof(f173_nnf,plain,
( ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)
& mtvisible(c_tptp_member974_mt) ),
inference(nnf_transformation,[status(thm)],[f173_neg]) ).
fof(f173_sk,plain,
( ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)
& mtvisible(c_tptp_member974_mt) ),
inference(skolemisation,[status(esa)],[f173_nnf]) ).
cnf(c174,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(cnf_transformation,[status(esa)],[f173_sk]) ).
cnf(hi174,negated_conjecture,
ifeq(disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c174]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi174,h766]) ).
cnf(t1388,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f64,axiom,
! [OBJ] :
~ ( tptpcol_1_65536(OBJ)
& tptpcol_1_1(OBJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just65) ).
fof(f64_nnf,plain,
! [OBJ] :
( ~ tptpcol_1_65536(OBJ)
| ~ tptpcol_1_1(OBJ) ),
inference(nnf_transformation,[status(thm)],[f64]) ).
fof(f64_sk,plain,
! [OBJ] :
( ~ tptpcol_1_65536(OBJ)
| ~ tptpcol_1_1(OBJ) ),
inference(skolemisation,[status(esa)],[f64_nnf]) ).
cnf(c64,plain,
( ~ tptpcol_1_65536(X0)
| ~ tptpcol_1_1(X0) ),
inference(cnf_transformation,[status(esa)],[f64_sk]) ).
fof(f67,axiom,
! [OBJ,COL1,COL2] :
~ ( disjointwith(COL1,COL2)
& isa(OBJ,COL2)
& isa(OBJ,COL1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',just68) ).
fof(f67_nnf,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(skolemisation,[status(esa)],[f67_nnf]) ).
cnf(c67,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X0,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c64,c67,c174]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1388]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR036+1 : 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.38 % Computer : n009.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Fri Sep 25 08:19:59 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 8.75/1.67 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.75/1.67 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------