%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR036+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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 : Tue Sep 29 09:44:30 AM UTC 2026
% Result : Theorem 41.12s 6.07s
% Output : Refutation 41.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 33
% Syntax : Number of formulae : 131 ( 91 unt; 0 def)
% Number of atoms : 179 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 92 ( 44 ~; 41 |; 3 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 32 con; 0-0 aty)
% Number of variables : 53 ( 53 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_6) ).
fof(f21,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_21) ).
fof(f26,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_26) ).
fof(f28,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_28) ).
fof(f30,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_30) ).
fof(f74,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_74) ).
fof(f145,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_145) ).
fof(f152,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_152) ).
fof(f168,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_168) ).
fof(f189,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_189) ).
fof(f193,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_193) ).
fof(f199,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_199) ).
fof(f224,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_224) ).
fof(f230,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_230) ).
fof(f280,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_280) ).
fof(f285,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_285) ).
fof(f305,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_305) ).
fof(f311,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_311) ).
fof(f335,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_335) ).
fof(f348,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_348) ).
fof(f385,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_385) ).
fof(f395,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_395) ).
fof(f397,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_397) ).
fof(f403,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_403) ).
fof(f405,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_405) ).
fof(f436,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_436) ).
fof(f442,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_442) ).
fof(f449,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_449) ).
fof(f456,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_456) ).
fof(f491,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_491) ).
fof(f1121,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X1) )
=> disjointwith(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_1121) ).
fof(f1122,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X0) )
=> disjointwith(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+1.ax',ax1_1122) ).
fof(f1132,conjecture,
( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query86) ).
fof(f1133,negated_conjecture,
~ ( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(negated_conjecture,[status(cth)],[f1132]) ).
fof(f2008,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(ennf_transformation,[],[f1121]) ).
fof(f2009,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(flattening,[],[f2008]) ).
fof(f2010,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(ennf_transformation,[],[f1122]) ).
fof(f2011,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(flattening,[],[f2010]) ).
fof(f2022,plain,
( ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795)
& mtvisible(c_tptp_member974_mt) ),
inference(ennf_transformation,[],[f1133]) ).
fof(f2028,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(cnf_transformation,[],[f6]) ).
fof(f2043,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(cnf_transformation,[],[f21]) ).
fof(f2048,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(cnf_transformation,[],[f26]) ).
fof(f2050,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(cnf_transformation,[],[f28]) ).
fof(f2052,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(cnf_transformation,[],[f30]) ).
fof(f2095,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(cnf_transformation,[],[f74]) ).
fof(f2166,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[],[f145]) ).
fof(f2173,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f152]) ).
fof(f2189,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(cnf_transformation,[],[f168]) ).
fof(f2210,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(cnf_transformation,[],[f189]) ).
fof(f2214,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(cnf_transformation,[],[f193]) ).
fof(f2220,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(cnf_transformation,[],[f199]) ).
fof(f2245,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(cnf_transformation,[],[f224]) ).
fof(f2251,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(cnf_transformation,[],[f230]) ).
fof(f2301,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(cnf_transformation,[],[f280]) ).
fof(f2306,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(cnf_transformation,[],[f285]) ).
fof(f2325,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(cnf_transformation,[],[f305]) ).
fof(f2331,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(cnf_transformation,[],[f311]) ).
fof(f2355,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(cnf_transformation,[],[f335]) ).
fof(f2368,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f348]) ).
fof(f2405,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[],[f385]) ).
fof(f2415,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(cnf_transformation,[],[f395]) ).
fof(f2417,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(cnf_transformation,[],[f397]) ).
fof(f2423,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(cnf_transformation,[],[f403]) ).
fof(f2425,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(cnf_transformation,[],[f405]) ).
fof(f2456,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(cnf_transformation,[],[f436]) ).
fof(f2462,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(cnf_transformation,[],[f442]) ).
fof(f2469,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(cnf_transformation,[],[f449]) ).
fof(f2476,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(cnf_transformation,[],[f456]) ).
fof(f2511,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(cnf_transformation,[],[f491]) ).
fof(f3051,plain,
! [X2,X0,X1] :
( ~ genls(X2,X1)
| ~ disjointwith(X0,X1)
| disjointwith(X0,X2) ),
inference(cnf_transformation,[],[f2009]) ).
fof(f3052,plain,
! [X2,X0,X1] :
( ~ genls(X2,X0)
| ~ disjointwith(X0,X1)
| disjointwith(X2,X1) ),
inference(cnf_transformation,[],[f2011]) ).
fof(f3063,plain,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(cnf_transformation,[],[f2022]) ).
fof(f5252,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_9_72709)
| disjointwith(X0,c_tptpcol_10_72710) ),
inference(resolution,[],[f3051,f2028]) ).
fof(f5253,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_8_72708)
| disjointwith(X0,c_tptpcol_9_72709) ),
inference(resolution,[],[f3051,f2220]) ).
fof(f5263,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_13_72791)
| disjointwith(X0,c_tptpcol_14_72792) ),
inference(resolution,[],[f3051,f2048]) ).
fof(f5264,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_12_72775)
| disjointwith(X0,c_tptpcol_13_72791) ),
inference(resolution,[],[f3051,f2511]) ).
fof(f5274,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_1_65536)
| disjointwith(X0,c_tptpcol_2_65537) ),
inference(resolution,[],[f3051,f2368]) ).
fof(f5289,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_7_72707)
| disjointwith(X0,c_tptpcol_8_72708) ),
inference(resolution,[],[f3051,f2095]) ).
fof(f5290,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_6_71683)
| disjointwith(X0,c_tptpcol_7_72707) ),
inference(resolution,[],[f3051,f2417]) ).
fof(f5339,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_4_65539)
| disjointwith(X0,c_tptpcol_5_69635) ),
inference(resolution,[],[f3051,f2245]) ).
fof(f5340,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_3_65538)
| disjointwith(X0,c_tptpcol_4_65539) ),
inference(resolution,[],[f3051,f2456]) ).
fof(f5353,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_14_72792)
| disjointwith(X0,c_tptpcol_15_72793) ),
inference(resolution,[],[f3051,f2301]) ).
fof(f5358,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_2_65537)
| disjointwith(X0,c_tptpcol_3_65538) ),
inference(resolution,[],[f3051,f2331]) ).
fof(f5377,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_11_72774)
| disjointwith(X0,c_tptpcol_12_72775) ),
inference(resolution,[],[f3051,f2415]) ).
fof(f5378,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_10_72710)
| disjointwith(X0,c_tptpcol_11_72774) ),
inference(resolution,[],[f3051,f2469]) ).
fof(f5379,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_5_69635)
| disjointwith(X0,c_tptpcol_6_71683) ),
inference(resolution,[],[f3051,f2425]) ).
fof(f5382,plain,
! [X0] :
( ~ disjointwith(X0,c_tptpcol_15_72793)
| disjointwith(X0,c_tptpcol_16_72795) ),
inference(resolution,[],[f3051,f2423]) ).
fof(f5405,plain,
! [X0] :
( ~ disjointwith(c_tptpcol_8_22020,X0)
| disjointwith(c_tptpcol_9_22021,X0) ),
inference(resolution,[],[f3052,f2043]) ).
fof(f5406,plain,
! [X0] :
( ~ disjointwith(c_tptpcol_7_21508,X0)
| disjointwith(c_tptpcol_8_22020,X0) ),
inference(resolution,[],[f3052,f2325]) ).
fof(f5408,plain,
! [X0] :
( ~ disjointwith(c_tptpcol_3_16386,X0)
| disjointwith(c_tptpcol_4_16387,X0) ),
inference(resolution,[],[f3052,f2306]) ).
fof(f5411,plain,
! [X0] :
( ~ disjointwith(c_tptpcol_4_16387,X0)
| disjointwith(c_tptpcol_5_20483,X0) ),
inference(resolution,[],[f3052,f2050]) ).
fof(f5412,plain,
! [X0] :
( ~ disjointwith(c_tptpcol_10_22022,X0)
| disjointwith(c_tptpcol_11_22023,X0) ),
inference(resolution,[],[f3052,f2052]) ).
fof(f5413,plain,
! [X0] :
( ~ disjointwith(c_tptpcol_9_22021,X0)
| disjointwith(c_tptpcol_10_22022,X0) ),
inference(resolution,[],[f3052,f2214]) ).
fof(f5461,plain,
! [X0] :
( ~ disjointwith(c_tptpcol_1_1,X0)
| disjointwith(c_tptpcol_2_2,X0) ),
inference(resolution,[],[f3052,f2166]) ).
fof(f5469,plain,
! [X0] :
( ~ disjointwith(c_tptpcol_11_22023,X0)
| disjointwith(c_tptpcol_12_22055,X0) ),
inference(resolution,[],[f3052,f2189]) ).
fof(f5475,plain,
! [X0] :
( ~ disjointwith(c_tptpcol_13_22071,X0)
| disjointwith(c_tptpcol_14_22072,X0) ),
inference(resolution,[],[f3052,f2210]) ).
fof(f5476,plain,
! [X0] :
( ~ disjointwith(c_tptpcol_12_22055,X0)
| disjointwith(c_tptpcol_13_22071,X0) ),
inference(resolution,[],[f3052,f2251]) ).
fof(f5484,plain,
! [X0] :
( ~ disjointwith(c_tptpcol_2_2,X0)
| disjointwith(c_tptpcol_3_16386,X0) ),
inference(resolution,[],[f3052,f2405]) ).
fof(f5503,plain,
! [X0] :
( ~ disjointwith(c_tptpcol_6_20484,X0)
| disjointwith(c_tptpcol_7_21508,X0) ),
inference(resolution,[],[f3052,f2476]) ).
fof(f5511,plain,
! [X0] :
( ~ disjointwith(c_tptpcol_5_20483,X0)
| disjointwith(c_tptpcol_6_20484,X0) ),
inference(resolution,[],[f3052,f2355]) ).
fof(f5534,plain,
! [X0] :
( ~ disjointwith(c_tptpcol_14_22072,X0)
| disjointwith(c_tptpcol_15_22076,X0) ),
inference(resolution,[],[f3052,f2462]) ).
fof(f9588,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_2_65537),
inference(resolution,[],[f5274,f2173]) ).
fof(f55217,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_2_65537),
inference(resolution,[],[f9588,f5461]) ).
fof(f58328,plain,
disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537),
inference(resolution,[],[f55217,f5484]) ).
fof(f90874,plain,
disjointwith(c_tptpcol_4_16387,c_tptpcol_2_65537),
inference(resolution,[],[f58328,f5408]) ).
fof(f94038,plain,
disjointwith(c_tptpcol_5_20483,c_tptpcol_2_65537),
inference(resolution,[],[f90874,f5411]) ).
fof(f97380,plain,
disjointwith(c_tptpcol_6_20484,c_tptpcol_2_65537),
inference(resolution,[],[f94038,f5511]) ).
fof(f100735,plain,
disjointwith(c_tptpcol_7_21508,c_tptpcol_2_65537),
inference(resolution,[],[f97380,f5503]) ).
fof(f104256,plain,
disjointwith(c_tptpcol_8_22020,c_tptpcol_2_65537),
inference(resolution,[],[f100735,f5406]) ).
fof(f108008,plain,
disjointwith(c_tptpcol_9_22021,c_tptpcol_2_65537),
inference(resolution,[],[f104256,f5405]) ).
fof(f112021,plain,
disjointwith(c_tptpcol_10_22022,c_tptpcol_2_65537),
inference(resolution,[],[f108008,f5413]) ).
fof(f116385,plain,
disjointwith(c_tptpcol_11_22023,c_tptpcol_2_65537),
inference(resolution,[],[f112021,f5412]) ).
fof(f121103,plain,
disjointwith(c_tptpcol_12_22055,c_tptpcol_2_65537),
inference(resolution,[],[f116385,f5469]) ).
fof(f126210,plain,
disjointwith(c_tptpcol_13_22071,c_tptpcol_2_65537),
inference(resolution,[],[f121103,f5476]) ).
fof(f131659,plain,
disjointwith(c_tptpcol_14_22072,c_tptpcol_2_65537),
inference(resolution,[],[f126210,f5475]) ).
fof(f137308,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_2_65537),
inference(resolution,[],[f131659,f5534]) ).
fof(f143129,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_3_65538),
inference(resolution,[],[f137308,f5358]) ).
fof(f149054,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_4_65539),
inference(resolution,[],[f143129,f5340]) ).
fof(f155067,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_5_69635),
inference(resolution,[],[f149054,f5339]) ).
fof(f160911,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_6_71683),
inference(resolution,[],[f155067,f5379]) ).
fof(f166317,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_7_72707),
inference(resolution,[],[f160911,f5290]) ).
fof(f171468,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_8_72708),
inference(resolution,[],[f166317,f5289]) ).
fof(f176125,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_9_72709),
inference(resolution,[],[f171468,f5253]) ).
fof(f180062,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_10_72710),
inference(resolution,[],[f176125,f5252]) ).
fof(f183492,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_11_72774),
inference(resolution,[],[f180062,f5378]) ).
fof(f186436,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_12_72775),
inference(resolution,[],[f183492,f5377]) ).
fof(f188899,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_13_72791),
inference(resolution,[],[f186436,f5264]) ).
fof(f190907,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_14_72792),
inference(resolution,[],[f188899,f5263]) ).
fof(f192516,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_15_72793),
inference(resolution,[],[f190907,f5353]) ).
fof(f193714,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(resolution,[],[f192516,f5382]) ).
fof(f193719,plain,
$false,
inference(forward_subsumption_resolution,[],[f193714,f3063]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR036+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n011.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 22:14:08 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.04/2.54 % (3840288)Will run a generic schedule for satisfiability detection.
% 16.04/2.54 % (3840297)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3120552541:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 16.04/2.54 % (3840294)% WARNING: option uhcvi not known.
% 16.04/2.54 % (3840293)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3344364358_2999 on theBenchmark for (2999ds/0Mi)
% 16.04/2.54 % (3840294)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=442695807:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 16.04/2.54 % (3840295)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=65368787:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 16.04/2.54 % (3840296)dis+10_1_sil=32000:sp=arity:random_seed=2777997723:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 16.04/2.54 % (3840298)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1218330594:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 16.04/2.54 % (3840299)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3247682117:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 16.04/2.54 % TRYING [1]
% 16.04/2.54 % (3840297)Instruction limit reached!
% 16.04/2.54 % (3840297)------------------------------
% 16.04/2.54 % (3840297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.04/2.54 % (3840297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.04/2.54 % (3840297)CaDiCaL version: 2.1.3
% 16.04/2.54 % (3840297)Termination reason: Instruction limit
% 16.04/2.54 % (3840297)Termination phase: Saturation
% 16.04/2.54 % (3840297)Time elapsed: 0.035 s
% 16.04/2.54 % (3840297)Peak memory usage: 15 MB
% 16.04/2.54 % (3840297)Instructions burned: 117 (million)
% 16.04/2.54 % TRYING [2]
% 16.04/2.54 % TRYING [3]
% 16.04/2.54 % (3840307)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2844374159:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 16.04/2.54 % TRYING [4]
% 16.04/2.54 % TRYING [1]
% 16.04/2.54 % TRYING [2]
% 16.04/2.54 % (3840296)Instruction limit reached!
% 16.04/2.54 % (3840296)------------------------------
% 16.04/2.54 % (3840296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.04/2.54 % (3840296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.04/2.54 % (3840296)CaDiCaL version: 2.1.3
% 16.04/2.54 % (3840296)Termination reason: Instruction limit
% 16.04/2.54 % (3840296)Termination phase: Saturation
% 16.04/2.54 % (3840296)Time elapsed: 0.055 s
% 16.04/2.54 % (3840296)Peak memory usage: 15 MB
% 16.04/2.54 % (3840296)Instructions burned: 103 (million)
% 16.04/2.54 % TRYING [3]
% 16.04/2.54 % TRYING [4]
% 16.04/2.54 % (3840298)Instruction limit reached!
% 16.04/2.54 % (3840298)------------------------------
% 16.04/2.54 % (3840298)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.04/2.54 % (3840298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.04/2.54 % (3840298)CaDiCaL version: 2.1.3
% 16.04/2.54 % (3840298)Termination reason: Instruction limit
% 16.04/2.54 % (3840298)Termination phase: Saturation
% 16.04/2.54 % (3840298)Time elapsed: 0.075 s
% 16.04/2.54 % (3840298)Peak memory usage: 16 MB
% 16.04/2.54 % (3840298)Instructions burned: 132 (million)
% 16.04/2.54 % (3840309)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3320483322:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 16.04/2.54 % TRYING [5]
% 16.04/2.54 % TRYING [5]
% 16.04/2.54 % (3840299)Instruction limit reached!
% 16.04/2.54 % (3840299)------------------------------
% 16.04/2.54 % (3840299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.04/2.54 % (3840299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.04/2.54 % (3840299)CaDiCaL version: 2.1.3
% 16.04/2.54 % (3840299)Termination reason: Instruction limit
% 16.04/2.54 % (3840299)Termination phase: Saturation
% 16.04/2.54 % (3840299)Time elapsed: 0.087 s
% 16.04/2.54 % (3840299)Peak memory usage: 17 MB
% 16.04/2.54 % (3840299)Instructions burned: 160 (million)
% 16.04/2.54 % (3840311)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3567475243:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 16.04/2.54 % (3840312)ott-21_1_sil=16000:fs=off:random_seed=1513980844:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 16.04/2.54 % TRYING [6]
% 16.04/2.54 % (3840309)Instruction limit reached!
% 16.04/2.54 % (3840309)------------------------------
% 16.04/2.54 % (3840309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.33/5.53 % (3840309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.33/5.53 % (3840309)CaDiCaL version: 2.1.3
% 37.33/5.53 % (3840309)Termination reason: Instruction limit
% 37.33/5.53 % (3840309)Termination phase: Saturation
% 37.33/5.53 % (3840309)Time elapsed: 0.069 s
% 37.33/5.53 % (3840309)Peak memory usage: 16 MB
% 37.33/5.53 % (3840309)Instructions burned: 131 (million)
% 37.33/5.53 % TRYING [6]
% 37.33/5.53 % (3840315)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3548805971:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 37.33/5.53 % (3840307)Instruction limit reached!
% 37.33/5.53 % (3840307)------------------------------
% 37.33/5.53 % (3840307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.33/5.53 % (3840307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.33/5.53 % (3840307)CaDiCaL version: 2.1.3
% 37.33/5.53 % (3840307)Termination reason: Instruction limit
% 37.33/5.53 % (3840307)Termination phase: Finite model building SAT solving
% 37.33/5.53 % (3840307)Time elapsed: 0.158 s
% 37.33/5.53 % (3840307)Peak memory usage: 36 MB
% 37.33/5.53 % (3840307)Instructions burned: 719 (million)
% 37.33/5.53 % (3840312)Instruction limit reached!
% 37.33/5.53 % (3840312)------------------------------
% 37.33/5.53 % (3840312)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.33/5.53 % (3840312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.33/5.53 % (3840312)CaDiCaL version: 2.1.3
% 37.33/5.53 % (3840312)Termination reason: Instruction limit
% 37.33/5.53 % (3840312)Termination phase: Saturation
% 37.33/5.53 % (3840312)Time elapsed: 0.088 s
% 37.33/5.53 % (3840312)Peak memory usage: 16 MB
% 37.33/5.53 % (3840312)Instructions burned: 181 (million)
% 37.33/5.53 % (3840318)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1654832991:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 37.33/5.53 % (3840317)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4148293870:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 37.33/5.53 % TRYING [1]
% 37.33/5.53 % TRYING [2]
% 37.33/5.53 % TRYING [3]
% 37.33/5.53 % TRYING [4]
% 37.33/5.53 % (3840315)Instruction limit reached!
% 37.33/5.53 % (3840315)------------------------------
% 37.33/5.53 % (3840315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.33/5.53 % (3840315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.33/5.53 % (3840315)CaDiCaL version: 2.1.3
% 37.33/5.53 % (3840315)Termination reason: Instruction limit
% 37.33/5.53 % (3840315)Termination phase: Saturation
% 37.33/5.53 % (3840315)Time elapsed: 0.271 s
% 37.33/5.53 % (3840315)Peak memory usage: 19 MB
% 37.33/5.53 % (3840315)Instructions burned: 478 (million)
% 37.33/5.53 % (3840321)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2557191841:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 37.33/5.53 % TRYING [7]
% 37.33/5.53 % (3840311)Instruction limit reached!
% 37.33/5.53 % (3840311)------------------------------
% 37.33/5.53 % (3840311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.33/5.53 % (3840311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.33/5.53 % (3840311)CaDiCaL version: 2.1.3
% 37.33/5.53 % (3840311)Termination reason: Instruction limit
% 37.33/5.53 % (3840311)Termination phase: Saturation
% 37.33/5.53 % (3840311)Time elapsed: 0.390 s
% 37.33/5.53 % (3840311)Peak memory usage: 22 MB
% 37.33/5.53 % (3840311)Instructions burned: 686 (million)
% 37.33/5.53 % (3840318)Instruction limit reached!
% 37.33/5.53 % (3840318)------------------------------
% 37.33/5.53 % (3840318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.33/5.53 % (3840318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.33/5.53 % (3840318)CaDiCaL version: 2.1.3
% 37.33/5.53 % (3840318)Termination reason: Instruction limit
% 37.33/5.53 % (3840318)Termination phase: Saturation
% 37.33/5.53 % (3840318)Time elapsed: 0.294 s
% 37.33/5.53 % (3840318)Peak memory usage: 34 MB
% 37.33/5.53 % (3840318)Instructions burned: 1181 (million)
% 37.33/5.53 % (3840323)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1448455243:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 37.33/5.53 % (3840324)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3693181789:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 37.33/5.53 % TRYING [5]
% 37.33/5.53 % (3840317)Instruction limit reached!
% 37.33/5.53 % (3840317)------------------------------
% 41.12/6.07 % (3840317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.12/6.07 % (3840317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.12/6.07 % (3840317)CaDiCaL version: 2.1.3
% 41.12/6.07 % (3840317)Termination reason: Instruction limit
% 41.12/6.07 % (3840317)Termination phase: Finite model building constraint generation
% 41.12/6.07 % (3840317)Time elapsed: 0.353 s
% 41.12/6.07 % (3840317)Peak memory usage: 23 MB
% 41.12/6.07 % (3840317)Instructions burned: 865 (million)
% 41.12/6.07 % (3840327)fmb+10_1_sil=64000:random_seed=564085245:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 41.12/6.07 % TRYING [1]
% 41.12/6.07 % TRYING [2]
% 41.12/6.07 % TRYING [3]
% 41.12/6.07 % TRYING [4]
% 41.12/6.07 % (3840324)Instruction limit reached!
% 41.12/6.07 % (3840324)------------------------------
% 41.12/6.07 % (3840324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.12/6.07 % (3840324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.12/6.07 % (3840324)CaDiCaL version: 2.1.3
% 41.12/6.07 % (3840324)Termination reason: Instruction limit
% 41.12/6.07 % (3840324)Termination phase: Saturation
% 41.12/6.07 % (3840324)Time elapsed: 0.199 s
% 41.12/6.07 % (3840324)Peak memory usage: 19 MB
% 41.12/6.07 % (3840324)Instructions burned: 882 (million)
% 41.12/6.07 % (3840329)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4238773509:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 41.12/6.07 % TRYING [20]
% 41.12/6.07 % TRYING [5]
% 41.12/6.07 % (3840321)Instruction limit reached!
% 41.12/6.07 % (3840321)------------------------------
% 41.12/6.07 % (3840321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.12/6.07 % (3840321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.12/6.07 % (3840321)CaDiCaL version: 2.1.3
% 41.12/6.07 % (3840321)Termination reason: Instruction limit
% 41.12/6.07 % (3840321)Termination phase: Finite model building constraint generation
% 41.12/6.07 % (3840321)Time elapsed: 0.414 s
% 41.12/6.07 % (3840321)Peak memory usage: 102 MB
% 41.12/6.07 % (3840321)Instructions burned: 890 (million)
% 41.12/6.07 % (3840331)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2909320931:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 41.12/6.07 % (3840323)Instruction limit reached!
% 41.12/6.07 % (3840323)------------------------------
% 41.12/6.07 % (3840323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.12/6.07 % (3840323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.12/6.07 % (3840323)CaDiCaL version: 2.1.3
% 41.12/6.07 % (3840323)Termination reason: Instruction limit
% 41.12/6.07 % (3840323)Termination phase: Saturation
% 41.12/6.07 % (3840323)Time elapsed: 0.411 s
% 41.12/6.07 % (3840323)Peak memory usage: 26 MB
% 41.12/6.07 % (3840323)Instructions burned: 693 (million)
% 41.12/6.07 % TRYING [8]
% 41.12/6.07 % (3840333)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1851281167:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 41.12/6.07 % TRYING [6]
% 41.12/6.07 % (3840331)Instruction limit reached!
% 41.12/6.07 % (3840331)------------------------------
% 41.12/6.07 % (3840331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.12/6.07 % (3840331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.12/6.07 % (3840331)CaDiCaL version: 2.1.3
% 41.12/6.07 % (3840331)Termination reason: Instruction limit
% 41.12/6.07 % (3840331)Termination phase: Finite model building SAT solving
% 41.12/6.07 % (3840331)Time elapsed: 0.438 s
% 41.12/6.07 % (3840331)Peak memory usage: 81 MB
% 41.12/6.07 % (3840331)Instructions burned: 920 (million)
% 41.12/6.07 % (3840335)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2058034179:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 41.12/6.07 % TRYING [7]
% 41.12/6.07 % (3840335)Instruction limit reached!
% 41.12/6.07 % (3840335)------------------------------
% 41.12/6.07 % (3840335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.12/6.07 % (3840335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.12/6.07 % (3840335)CaDiCaL version: 2.1.3
% 41.12/6.07 % (3840335)Termination reason: Instruction limit
% 41.12/6.07 % (3840335)Termination phase: Saturation
% 41.12/6.07 % (3840335)Time elapsed: 0.869 s
% 41.12/6.07 % (3840335)Peak memory usage: 29 MB
% 41.12/6.07 % (3840335)Instructions burned: 1473 (million)
% 41.12/6.07 % (3840337)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=242213859:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 41.12/6.07 % (3840337)Cannot represent all propositional literals internally
% 41.12/6.07 % (3840337)Refutation not found, incomplete strategy
% 41.12/6.07 % (3840337)------------------------------
% 41.12/6.07 % (3840337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.12/6.07 % (3840337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.12/6.07 % (3840337)CaDiCaL version: 2.1.3
% 41.12/6.07 % (3840337)Termination reason: Refutation not found, incomplete strategy
% 41.12/6.07 % (3840337)Time elapsed: 0.027 s
% 41.12/6.07 % (3840337)Peak memory usage: 13 MB
% 41.12/6.07 % (3840337)Instructions burned: 55 (million)
% 41.12/6.07 % (3840337)------------------------------
% 41.12/6.07 % (3840337)------------------------------
% 41.12/6.07 % (3840339)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=241984813:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi)
% 41.12/6.07 % TRYING [16]
% 41.12/6.07 % (3840339)Instruction limit reached!
% 41.12/6.07 % (3840339)------------------------------
% 41.12/6.07 % (3840339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.12/6.07 % (3840339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.12/6.07 % (3840339)CaDiCaL version: 2.1.3
% 41.12/6.07 % (3840339)Termination reason: Instruction limit
% 41.12/6.07 % (3840339)Termination phase: Finite model building constraint generation
% 41.12/6.07 % (3840339)Time elapsed: 0.781 s
% 41.12/6.07 % (3840339)Peak memory usage: 152 MB
% 41.12/6.07 % (3840339)Instructions burned: 2176 (million)
% 41.12/6.07 % (3840341)ott-2_1_sil=16000:newcnf=on:random_seed=608052215:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2968 on theBenchmark for (2968ds/869Mi)
% 41.12/6.07 % (3840333)Instruction limit reached!
% 41.12/6.07 % (3840333)------------------------------
% 41.12/6.07 % (3840333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.12/6.07 % (3840333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.12/6.07 % (3840333)CaDiCaL version: 2.1.3
% 41.12/6.07 % (3840333)Termination reason: Instruction limit
% 41.12/6.07 % (3840333)Termination phase: Saturation
% 41.12/6.07 % (3840333)Time elapsed: 2.367 s
% 41.12/6.07 % (3840333)Peak memory usage: 54 MB
% 41.12/6.07 % (3840333)Instructions burned: 5133 (million)
% 41.12/6.07 % (3840343)ott+10_1_sil=32000:tgt=ground:random_seed=2704612925:i=5114:av=off_2966 on theBenchmark for (2966ds/5114Mi)
% 41.12/6.07 % (3840329)Instruction limit reached!
% 41.12/6.07 % (3840329)------------------------------
% 41.12/6.07 % (3840329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.12/6.07 % (3840329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.12/6.07 % (3840329)CaDiCaL version: 2.1.3
% 41.12/6.07 % (3840329)Termination reason: Instruction limit
% 41.12/6.07 % (3840329)Termination phase: Finite model building constraint generation
% 41.12/6.07 % (3840329)Time elapsed: 2.645 s
% 41.12/6.07 % (3840329)Peak memory usage: 1541 MB
% 41.12/6.07 % (3840329)Instructions burned: 9516 (million)
% 41.12/6.07 % (3840345)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3424842149:i=54282_2964 on theBenchmark for (2964ds/54282Mi)
% 41.12/6.07 % TRYING [1]
% 41.12/6.07 % TRYING [2]
% 41.12/6.07 % TRYING [3]
% 41.12/6.07 % TRYING [4]
% 41.12/6.07 % TRYING [5]
% 41.12/6.07 % TRYING [6]
% 41.12/6.07 % (3840341)Instruction limit reached!
% 41.12/6.07 % (3840341)------------------------------
% 41.12/6.07 % (3840341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.12/6.07 % (3840341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.12/6.07 % (3840341)CaDiCaL version: 2.1.3
% 41.12/6.07 % (3840341)Termination reason: Instruction limit
% 41.12/6.07 % (3840341)Termination phase: Saturation
% 41.12/6.07 % (3840341)Time elapsed: 0.451 s
% 41.12/6.07 % (3840341)Peak memory usage: 42 MB
% 41.12/6.07 % (3840341)Instructions burned: 870 (million)
% 41.12/6.07 % (3840347)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=719667939:i=3512:aac=none_2963 on theBenchmark for (2963ds/3512Mi)
% 41.12/6.07 % TRYING [7]
% 41.12/6.07 % (3840347)Instruction limit reached!
% 41.12/6.07 % (3840347)------------------------------
% 41.12/6.07 % (3840347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.12/6.07 % (3840347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.12/6.07 % (3840347)CaDiCaL version: 2.1.3
% 41.12/6.07 % (3840347)Termination reason: Instruction limit
% 41.12/6.07 % (3840347)Termination phase: Saturation
% 41.12/6.07 % (3840347)Time elapsed: 1.640 s
% 41.12/6.07 % (3840347)Peak memory usage: 104 MB
% 41.12/6.07 % (3840347)Instructions burned: 3512 (million)
% 41.12/6.07 % (3840349)dis+21_1_sil=32000:sas=cadical:random_seed=2520993922:i=3773:amm=off_2946 on theBenchmark for (2946ds/3773Mi)
% 41.12/6.07 % (3840343) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3840288-3840343"...
% 41.12/6.07 % (3840343)...printing done.
% 41.12/6.07 % (3840343)Refutation found. Thanks to Tanya!
% 41.12/6.07 % SZS status Theorem for theBenchmark
% 41.12/6.07 % SZS output start Proof for theBenchmark
% See solution above
% 41.12/6.08 % (3840343)------------------------------
% 41.12/6.08 % (3840343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.12/6.08 % (3840343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.12/6.08 % (3840343)CaDiCaL version: 2.1.3
% 41.12/6.08 % (3840343)Termination reason: Refutation
% 41.12/6.08 % (3840343)Time elapsed: 2.427 s
% 41.12/6.08 % (3840343)Peak memory usage: 95 MB
% 41.12/6.08 % (3840343)Instructions burned: 4245 (million)
% 41.12/6.08 % (3840288)Success in time 5.848 s
% 41.12/6.08 % Vampire exiting
%------------------------------------------------------------------------------