%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR024+1.010 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n020.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 : Sun Sep 27 07:06:34 AM UTC 2026
% Result : Theorem 24.88s 3.55s
% Output : CNFRefutation 24.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 6
% Syntax : Number of formulae : 182 ( 86 unt; 0 def)
% Number of atoms : 411 ( 162 equ)
% Maximal formula atoms : 41 ( 2 avg)
% Number of connectives : 402 ( 173 ~; 181 |; 45 &)
% ( 2 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 28 ( 28 usr; 22 con; 0-2 aty)
% Number of variables : 108 ( 0 sgn 8 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(happens_holds,axiom,
! [Event,Time,Fluent] :
( ( initiates(Event,Fluent,Time)
& happens(Event,Time) )
=> holdsAt(Fluent,plus(Time,n1)) ),
file('theBenchmark.p',happens_holds) ).
fof(initiates_all_defn,axiom,
! [Event,Fluent,Time] :
( initiates(Event,Fluent,Time)
<=> ? [Agent,Trolley] :
( ( happens(push(Agent,Trolley),Time)
& Fluent = spinning(Trolley)
& Event = pull(Agent,Trolley) )
| ( ~ happens(push(Agent,Trolley),Time)
& Fluent = backwards(Trolley)
& Event = pull(Agent,Trolley) )
| ( ~ happens(pull(Agent,Trolley),Time)
& Fluent = forwards(Trolley)
& Event = push(Agent,Trolley) ) ) ),
file('theBenchmark.p',initiates_all_defn) ).
fof(happens_all_defn,axiom,
! [Event,Time] :
( happens(Event,Time)
<=> ( ( Time = n0
& Event = push(agent10,trolley10) )
| ( Time = n0
& Event = pull(agent10,trolley10) )
| ( Time = n0
& Event = push(agent9,trolley9) )
| ( Time = n0
& Event = pull(agent9,trolley9) )
| ( Time = n0
& Event = push(agent8,trolley8) )
| ( Time = n0
& Event = pull(agent8,trolley8) )
| ( Time = n0
& Event = push(agent7,trolley7) )
| ( Time = n0
& Event = pull(agent7,trolley7) )
| ( Time = n0
& Event = push(agent6,trolley6) )
| ( Time = n0
& Event = pull(agent6,trolley6) )
| ( Time = n0
& Event = push(agent5,trolley5) )
| ( Time = n0
& Event = pull(agent5,trolley5) )
| ( Time = n0
& Event = push(agent4,trolley4) )
| ( Time = n0
& Event = pull(agent4,trolley4) )
| ( Time = n0
& Event = push(agent3,trolley3) )
| ( Time = n0
& Event = pull(agent3,trolley3) )
| ( Time = n0
& Event = push(agent2,trolley2) )
| ( Time = n0
& Event = pull(agent2,trolley2) )
| ( Time = n0
& Event = push(agent1,trolley1) )
| ( Time = n0
& Event = pull(agent1,trolley1) ) ) ),
file('theBenchmark.p',happens_all_defn) ).
fof(spinning_3,conjecture,
( holdsAt(spinning(trolley10),n1)
& holdsAt(spinning(trolley9),n1)
& holdsAt(spinning(trolley8),n1)
& holdsAt(spinning(trolley7),n1)
& holdsAt(spinning(trolley6),n1)
& holdsAt(spinning(trolley5),n1)
& holdsAt(spinning(trolley4),n1)
& holdsAt(spinning(trolley3),n1)
& holdsAt(spinning(trolley2),n1)
& holdsAt(spinning(trolley1),n1) ),
file('theBenchmark.p',spinning_3) ).
fof(spinning_3_neg,negated_conjecture,
~ ( holdsAt(spinning(trolley10),n1)
& holdsAt(spinning(trolley9),n1)
& holdsAt(spinning(trolley8),n1)
& holdsAt(spinning(trolley7),n1)
& holdsAt(spinning(trolley6),n1)
& holdsAt(spinning(trolley5),n1)
& holdsAt(spinning(trolley4),n1)
& holdsAt(spinning(trolley3),n1)
& holdsAt(spinning(trolley2),n1)
& holdsAt(spinning(trolley1),n1) ),
inference(assume_negation,[status(cth)],[spinning_3]) ).
cnf(c_134,plain,
( n0 != B
| push(agent10,trolley10) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_135,plain,
( n0 != B
| pull(agent10,trolley10) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_136,plain,
( n0 != B
| push(agent9,trolley9) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_137,plain,
( n0 != B
| pull(agent9,trolley9) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_138,plain,
( n0 != B
| push(agent8,trolley8) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_139,plain,
( n0 != B
| pull(agent8,trolley8) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_140,plain,
( n0 != B
| push(agent7,trolley7) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_141,plain,
( n0 != B
| pull(agent7,trolley7) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_142,plain,
( n0 != B
| push(agent6,trolley6) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_143,plain,
( n0 != B
| pull(agent6,trolley6) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_144,plain,
( n0 != B
| push(agent5,trolley5) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_145,plain,
( n0 != B
| pull(agent5,trolley5) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_146,plain,
( n0 != B
| push(agent4,trolley4) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_147,plain,
( n0 != B
| pull(agent4,trolley4) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_148,plain,
( n0 != B
| push(agent3,trolley3) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_149,plain,
( n0 != B
| pull(agent3,trolley3) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_150,plain,
( n0 != B
| push(agent2,trolley2) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_151,plain,
( n0 != B
| pull(agent2,trolley2) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_152,plain,
( n0 != B
| push(agent1,trolley1) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_153,plain,
( n0 != B
| pull(agent1,trolley1) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
fof(plus0_1,axiom,
plus(n0,n1) = n1,
file('theBenchmark.p',plus0_1) ).
cnf(c_188,plain,
plus(n0,n1) = n1,
inference(clausify,[status(thm)],[plus0_1]) ).
fof(plus0_0,axiom,
plus(n0,n0) = n0,
file('theBenchmark.p',plus0_0) ).
cnf(c_189,plain,
plus(n0,n0) = n0,
inference(clausify,[status(thm)],[plus0_0]) ).
cnf(c_213,plain,
( ~ happens(push(D,E),C)
| spinning(E) != B
| pull(D,E) != A
| initiates(A,B,C) ),
inference(clausify,[status(thm)],[initiates_all_defn]) ).
cnf(c_231,plain,
( holdsAt(C,plus(B,n1))
| ~ initiates(A,C,B)
| ~ happens(A,B) ),
inference(clausify,[status(thm)],[happens_holds]) ).
cnf(c_398,negated_conjecture,
( ~ holdsAt(spinning(trolley10),n1)
| ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(clausify,[status(thm)],[spinning_3_neg]) ).
cnf(c_442,plain,
( n0 != A
| happens(push(agent10,trolley10),A) ),
inference(xxres,[status(thm)],[c_134]) ).
cnf(c_444,plain,
( n0 != A
| happens(pull(agent10,trolley10),A) ),
inference(xxres,[status(thm)],[c_135]) ).
cnf(c_446,plain,
( n0 != A
| happens(push(agent9,trolley9),A) ),
inference(xxres,[status(thm)],[c_136]) ).
cnf(c_448,plain,
( n0 != A
| happens(pull(agent9,trolley9),A) ),
inference(xxres,[status(thm)],[c_137]) ).
cnf(c_450,plain,
( n0 != A
| happens(push(agent8,trolley8),A) ),
inference(xxres,[status(thm)],[c_138]) ).
cnf(c_452,plain,
( n0 != A
| happens(pull(agent8,trolley8),A) ),
inference(xxres,[status(thm)],[c_139]) ).
cnf(c_454,plain,
( n0 != A
| happens(push(agent7,trolley7),A) ),
inference(xxres,[status(thm)],[c_140]) ).
cnf(c_456,plain,
( n0 != A
| happens(pull(agent7,trolley7),A) ),
inference(xxres,[status(thm)],[c_141]) ).
cnf(c_458,plain,
( n0 != A
| happens(push(agent6,trolley6),A) ),
inference(xxres,[status(thm)],[c_142]) ).
cnf(c_460,plain,
( n0 != A
| happens(pull(agent6,trolley6),A) ),
inference(xxres,[status(thm)],[c_143]) ).
cnf(c_462,plain,
( n0 != A
| happens(push(agent5,trolley5),A) ),
inference(xxres,[status(thm)],[c_144]) ).
cnf(c_464,plain,
( n0 != A
| happens(pull(agent5,trolley5),A) ),
inference(xxres,[status(thm)],[c_145]) ).
cnf(c_466,plain,
( n0 != A
| happens(push(agent4,trolley4),A) ),
inference(xxres,[status(thm)],[c_146]) ).
cnf(c_468,plain,
( n0 != A
| happens(pull(agent4,trolley4),A) ),
inference(xxres,[status(thm)],[c_147]) ).
cnf(c_470,plain,
( n0 != A
| happens(push(agent3,trolley3),A) ),
inference(xxres,[status(thm)],[c_148]) ).
cnf(c_472,plain,
( n0 != A
| happens(pull(agent3,trolley3),A) ),
inference(xxres,[status(thm)],[c_149]) ).
cnf(c_474,plain,
( n0 != A
| happens(push(agent2,trolley2),A) ),
inference(xxres,[status(thm)],[c_150]) ).
cnf(c_476,plain,
( n0 != A
| happens(pull(agent2,trolley2),A) ),
inference(xxres,[status(thm)],[c_151]) ).
cnf(c_478,plain,
( n0 != A
| happens(push(agent1,trolley1),A) ),
inference(xxres,[status(thm)],[c_152]) ).
cnf(c_480,plain,
( n0 != A
| happens(pull(agent1,trolley1),A) ),
inference(xxres,[status(thm)],[c_153]) ).
cnf(c_1691,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1692,plain,
happens(push(agent10,trolley10),plus(n0,n0)),
inference(resolve,[status(thm)],[c_442,c_1691]) ).
cnf(c_515,plain,
happens(push(agent10,trolley10),n0),
inference(paramod,[status(thm)],[c_189,c_1692]) ).
cnf(c_1693,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1694,plain,
happens(pull(agent10,trolley10),plus(n0,n0)),
inference(resolve,[status(thm)],[c_444,c_1693]) ).
cnf(c_545,plain,
happens(pull(agent10,trolley10),n0),
inference(paramod,[status(thm)],[c_189,c_1694]) ).
cnf(c_1695,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1696,plain,
happens(push(agent9,trolley9),plus(n0,n0)),
inference(resolve,[status(thm)],[c_446,c_1695]) ).
cnf(c_558,plain,
happens(push(agent9,trolley9),n0),
inference(paramod,[status(thm)],[c_189,c_1696]) ).
cnf(c_1697,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1698,plain,
happens(pull(agent9,trolley9),plus(n0,n0)),
inference(resolve,[status(thm)],[c_448,c_1697]) ).
cnf(c_575,plain,
happens(pull(agent9,trolley9),n0),
inference(paramod,[status(thm)],[c_189,c_1698]) ).
cnf(c_1699,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1700,plain,
happens(push(agent8,trolley8),plus(n0,n0)),
inference(resolve,[status(thm)],[c_450,c_1699]) ).
cnf(c_590,plain,
happens(push(agent8,trolley8),n0),
inference(paramod,[status(thm)],[c_189,c_1700]) ).
cnf(c_1701,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1702,plain,
happens(pull(agent8,trolley8),plus(n0,n0)),
inference(resolve,[status(thm)],[c_452,c_1701]) ).
cnf(c_607,plain,
happens(pull(agent8,trolley8),n0),
inference(paramod,[status(thm)],[c_189,c_1702]) ).
cnf(c_1703,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1704,plain,
happens(push(agent7,trolley7),plus(n0,n0)),
inference(resolve,[status(thm)],[c_454,c_1703]) ).
cnf(c_620,plain,
happens(push(agent7,trolley7),n0),
inference(paramod,[status(thm)],[c_189,c_1704]) ).
cnf(c_1705,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1706,plain,
happens(pull(agent7,trolley7),plus(n0,n0)),
inference(resolve,[status(thm)],[c_456,c_1705]) ).
cnf(c_639,plain,
happens(pull(agent7,trolley7),n0),
inference(paramod,[status(thm)],[c_189,c_1706]) ).
cnf(c_1707,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1708,plain,
happens(push(agent6,trolley6),plus(n0,n0)),
inference(resolve,[status(thm)],[c_458,c_1707]) ).
cnf(c_652,plain,
happens(push(agent6,trolley6),n0),
inference(paramod,[status(thm)],[c_189,c_1708]) ).
cnf(c_1709,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1710,plain,
happens(pull(agent6,trolley6),plus(n0,n0)),
inference(resolve,[status(thm)],[c_460,c_1709]) ).
cnf(c_665,plain,
happens(pull(agent6,trolley6),n0),
inference(paramod,[status(thm)],[c_189,c_1710]) ).
cnf(c_1711,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1712,plain,
happens(push(agent5,trolley5),plus(n0,n0)),
inference(resolve,[status(thm)],[c_462,c_1711]) ).
cnf(c_680,plain,
happens(push(agent5,trolley5),n0),
inference(paramod,[status(thm)],[c_189,c_1712]) ).
cnf(c_1713,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1714,plain,
happens(pull(agent5,trolley5),plus(n0,n0)),
inference(resolve,[status(thm)],[c_464,c_1713]) ).
cnf(c_695,plain,
happens(pull(agent5,trolley5),n0),
inference(paramod,[status(thm)],[c_189,c_1714]) ).
cnf(c_698,plain,
( spinning(trolley10) != B
| pull(agent10,trolley10) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_515,c_213]) ).
cnf(c_701,plain,
( spinning(trolley9) != B
| pull(agent9,trolley9) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_558,c_213]) ).
cnf(c_704,plain,
( spinning(trolley8) != B
| pull(agent8,trolley8) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_590,c_213]) ).
cnf(c_1715,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1716,plain,
happens(push(agent4,trolley4),plus(n0,n0)),
inference(resolve,[status(thm)],[c_466,c_1715]) ).
cnf(c_707,plain,
happens(push(agent4,trolley4),n0),
inference(paramod,[status(thm)],[c_189,c_1716]) ).
cnf(c_708,plain,
( spinning(trolley7) != B
| pull(agent7,trolley7) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_620,c_213]) ).
cnf(c_711,plain,
( spinning(trolley6) != B
| pull(agent6,trolley6) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_652,c_213]) ).
cnf(c_714,plain,
( spinning(trolley5) != B
| pull(agent5,trolley5) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_680,c_213]) ).
cnf(c_717,plain,
( spinning(trolley4) != B
| pull(agent4,trolley4) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_707,c_213]) ).
cnf(c_1717,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1718,plain,
happens(pull(agent4,trolley4),plus(n0,n0)),
inference(resolve,[status(thm)],[c_468,c_1717]) ).
cnf(c_720,plain,
happens(pull(agent4,trolley4),n0),
inference(paramod,[status(thm)],[c_189,c_1718]) ).
cnf(c_1719,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1720,plain,
happens(push(agent3,trolley3),plus(n0,n0)),
inference(resolve,[status(thm)],[c_470,c_1719]) ).
cnf(c_722,plain,
happens(push(agent3,trolley3),n0),
inference(paramod,[status(thm)],[c_189,c_1720]) ).
cnf(c_723,plain,
( spinning(trolley3) != B
| pull(agent3,trolley3) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_722,c_213]) ).
cnf(c_1721,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1722,plain,
happens(pull(agent3,trolley3),plus(n0,n0)),
inference(resolve,[status(thm)],[c_472,c_1721]) ).
cnf(c_726,plain,
happens(pull(agent3,trolley3),n0),
inference(paramod,[status(thm)],[c_189,c_1722]) ).
cnf(c_1723,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1724,plain,
happens(push(agent2,trolley2),plus(n0,n0)),
inference(resolve,[status(thm)],[c_474,c_1723]) ).
cnf(c_727,plain,
happens(push(agent2,trolley2),n0),
inference(paramod,[status(thm)],[c_189,c_1724]) ).
cnf(c_728,plain,
( spinning(trolley2) != B
| pull(agent2,trolley2) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_727,c_213]) ).
cnf(c_1725,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1726,plain,
happens(pull(agent2,trolley2),plus(n0,n0)),
inference(resolve,[status(thm)],[c_476,c_1725]) ).
cnf(c_731,plain,
happens(pull(agent2,trolley2),n0),
inference(paramod,[status(thm)],[c_189,c_1726]) ).
cnf(c_1727,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1728,plain,
happens(push(agent1,trolley1),plus(n0,n0)),
inference(resolve,[status(thm)],[c_478,c_1727]) ).
cnf(c_732,plain,
happens(push(agent1,trolley1),n0),
inference(paramod,[status(thm)],[c_189,c_1728]) ).
cnf(c_733,plain,
( spinning(trolley1) != B
| pull(agent1,trolley1) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_732,c_213]) ).
cnf(c_1729,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_189]) ).
cnf(c_1730,plain,
happens(pull(agent1,trolley1),plus(n0,n0)),
inference(resolve,[status(thm)],[c_480,c_1729]) ).
cnf(c_736,plain,
happens(pull(agent1,trolley1),n0),
inference(paramod,[status(thm)],[c_189,c_1730]) ).
cnf(c_867,plain,
( spinning(trolley10) != A
| initiates(pull(agent10,trolley10),A,n0) ),
inference(xxres,[status(thm)],[c_698]) ).
cnf(c_877,plain,
( spinning(trolley9) != A
| initiates(pull(agent9,trolley9),A,n0) ),
inference(xxres,[status(thm)],[c_701]) ).
cnf(c_931,plain,
( spinning(trolley8) != A
| initiates(pull(agent8,trolley8),A,n0) ),
inference(xxres,[status(thm)],[c_704]) ).
cnf(c_942,plain,
( spinning(trolley7) != A
| initiates(pull(agent7,trolley7),A,n0) ),
inference(xxres,[status(thm)],[c_708]) ).
cnf(c_951,plain,
( spinning(trolley6) != A
| initiates(pull(agent6,trolley6),A,n0) ),
inference(xxres,[status(thm)],[c_711]) ).
cnf(c_1000,plain,
( spinning(trolley5) != A
| initiates(pull(agent5,trolley5),A,n0) ),
inference(xxres,[status(thm)],[c_714]) ).
cnf(c_1010,plain,
( spinning(trolley4) != A
| initiates(pull(agent4,trolley4),A,n0) ),
inference(xxres,[status(thm)],[c_717]) ).
cnf(c_1025,plain,
( spinning(trolley3) != A
| initiates(pull(agent3,trolley3),A,n0) ),
inference(xxres,[status(thm)],[c_723]) ).
cnf(c_1057,plain,
( spinning(trolley2) != A
| initiates(pull(agent2,trolley2),A,n0) ),
inference(xxres,[status(thm)],[c_728]) ).
cnf(c_1071,plain,
( spinning(trolley1) != A
| initiates(pull(agent1,trolley1),A,n0) ),
inference(xxres,[status(thm)],[c_733]) ).
cnf(c_1135,plain,
initiates(pull(agent10,trolley10),spinning(trolley10),n0),
inference(xxres,[status(thm)],[c_867]) ).
cnf(c_1731,plain,
( holdsAt(spinning(trolley10),plus(n0,n1))
| ~ happens(pull(agent10,trolley10),n0) ),
inference(resolve,[status(thm)],[c_1135,c_231]) ).
cnf(c_1732,plain,
( holdsAt(spinning(trolley10),n1)
| ~ happens(pull(agent10,trolley10),n0) ),
inference(paramod,[status(thm)],[c_188,c_1731]) ).
cnf(c_1140,plain,
holdsAt(spinning(trolley10),n1),
inference(resolve,[status(thm)],[c_545,c_1732]) ).
cnf(c_1153,negated_conjecture,
( ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(resolve,[status(thm)],[c_1140,c_398]) ).
cnf(c_1208,plain,
initiates(pull(agent9,trolley9),spinning(trolley9),n0),
inference(xxres,[status(thm)],[c_877]) ).
cnf(c_1733,plain,
( holdsAt(spinning(trolley9),plus(n0,n1))
| ~ happens(pull(agent9,trolley9),n0) ),
inference(resolve,[status(thm)],[c_1208,c_231]) ).
cnf(c_1734,plain,
( holdsAt(spinning(trolley9),n1)
| ~ happens(pull(agent9,trolley9),n0) ),
inference(paramod,[status(thm)],[c_188,c_1733]) ).
cnf(c_1222,plain,
holdsAt(spinning(trolley9),n1),
inference(resolve,[status(thm)],[c_575,c_1734]) ).
cnf(c_1235,negated_conjecture,
( ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(resolve,[status(thm)],[c_1222,c_1153]) ).
cnf(c_1298,plain,
initiates(pull(agent8,trolley8),spinning(trolley8),n0),
inference(xxres,[status(thm)],[c_931]) ).
cnf(c_1735,plain,
( holdsAt(spinning(trolley8),plus(n0,n1))
| ~ happens(pull(agent8,trolley8),n0) ),
inference(resolve,[status(thm)],[c_1298,c_231]) ).
cnf(c_1736,plain,
( holdsAt(spinning(trolley8),n1)
| ~ happens(pull(agent8,trolley8),n0) ),
inference(paramod,[status(thm)],[c_188,c_1735]) ).
cnf(c_1316,plain,
holdsAt(spinning(trolley8),n1),
inference(resolve,[status(thm)],[c_607,c_1736]) ).
cnf(c_1329,negated_conjecture,
( ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(resolve,[status(thm)],[c_1316,c_1235]) ).
cnf(c_1383,plain,
initiates(pull(agent7,trolley7),spinning(trolley7),n0),
inference(xxres,[status(thm)],[c_942]) ).
cnf(c_1737,plain,
( holdsAt(spinning(trolley7),plus(n0,n1))
| ~ happens(pull(agent7,trolley7),n0) ),
inference(resolve,[status(thm)],[c_1383,c_231]) ).
cnf(c_1738,plain,
( holdsAt(spinning(trolley7),n1)
| ~ happens(pull(agent7,trolley7),n0) ),
inference(paramod,[status(thm)],[c_188,c_1737]) ).
cnf(c_1384,plain,
holdsAt(spinning(trolley7),n1),
inference(resolve,[status(thm)],[c_639,c_1738]) ).
cnf(c_1397,negated_conjecture,
( ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(resolve,[status(thm)],[c_1384,c_1329]) ).
cnf(c_1434,plain,
initiates(pull(agent6,trolley6),spinning(trolley6),n0),
inference(xxres,[status(thm)],[c_951]) ).
cnf(c_1739,plain,
( holdsAt(spinning(trolley6),plus(n0,n1))
| ~ happens(pull(agent6,trolley6),n0) ),
inference(resolve,[status(thm)],[c_1434,c_231]) ).
cnf(c_1740,plain,
( holdsAt(spinning(trolley6),n1)
| ~ happens(pull(agent6,trolley6),n0) ),
inference(paramod,[status(thm)],[c_188,c_1739]) ).
cnf(c_1435,plain,
holdsAt(spinning(trolley6),n1),
inference(resolve,[status(thm)],[c_665,c_1740]) ).
cnf(c_1448,negated_conjecture,
( ~ holdsAt(spinning(trolley5),n1)
| ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(resolve,[status(thm)],[c_1435,c_1397]) ).
cnf(c_1485,plain,
initiates(pull(agent5,trolley5),spinning(trolley5),n0),
inference(xxres,[status(thm)],[c_1000]) ).
cnf(c_1741,plain,
( holdsAt(spinning(trolley5),plus(n0,n1))
| ~ happens(pull(agent5,trolley5),n0) ),
inference(resolve,[status(thm)],[c_1485,c_231]) ).
cnf(c_1742,plain,
( holdsAt(spinning(trolley5),n1)
| ~ happens(pull(agent5,trolley5),n0) ),
inference(paramod,[status(thm)],[c_188,c_1741]) ).
cnf(c_1486,plain,
holdsAt(spinning(trolley5),n1),
inference(resolve,[status(thm)],[c_695,c_1742]) ).
cnf(c_1499,negated_conjecture,
( ~ holdsAt(spinning(trolley4),n1)
| ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(resolve,[status(thm)],[c_1486,c_1448]) ).
cnf(c_1536,plain,
initiates(pull(agent4,trolley4),spinning(trolley4),n0),
inference(xxres,[status(thm)],[c_1010]) ).
cnf(c_1743,plain,
( holdsAt(spinning(trolley4),plus(n0,n1))
| ~ happens(pull(agent4,trolley4),n0) ),
inference(resolve,[status(thm)],[c_1536,c_231]) ).
cnf(c_1744,plain,
( holdsAt(spinning(trolley4),n1)
| ~ happens(pull(agent4,trolley4),n0) ),
inference(paramod,[status(thm)],[c_188,c_1743]) ).
cnf(c_1537,plain,
holdsAt(spinning(trolley4),n1),
inference(resolve,[status(thm)],[c_720,c_1744]) ).
cnf(c_1550,negated_conjecture,
( ~ holdsAt(spinning(trolley3),n1)
| ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(resolve,[status(thm)],[c_1537,c_1499]) ).
cnf(c_1587,plain,
initiates(pull(agent3,trolley3),spinning(trolley3),n0),
inference(xxres,[status(thm)],[c_1025]) ).
cnf(c_1745,plain,
( holdsAt(spinning(trolley3),plus(n0,n1))
| ~ happens(pull(agent3,trolley3),n0) ),
inference(resolve,[status(thm)],[c_1587,c_231]) ).
cnf(c_1746,plain,
( holdsAt(spinning(trolley3),n1)
| ~ happens(pull(agent3,trolley3),n0) ),
inference(paramod,[status(thm)],[c_188,c_1745]) ).
cnf(c_1588,plain,
holdsAt(spinning(trolley3),n1),
inference(resolve,[status(thm)],[c_726,c_1746]) ).
cnf(c_1601,negated_conjecture,
( ~ holdsAt(spinning(trolley2),n1)
| ~ holdsAt(spinning(trolley1),n1) ),
inference(resolve,[status(thm)],[c_1588,c_1550]) ).
cnf(c_1638,plain,
initiates(pull(agent2,trolley2),spinning(trolley2),n0),
inference(xxres,[status(thm)],[c_1057]) ).
cnf(c_1747,plain,
( holdsAt(spinning(trolley2),plus(n0,n1))
| ~ happens(pull(agent2,trolley2),n0) ),
inference(resolve,[status(thm)],[c_1638,c_231]) ).
cnf(c_1748,plain,
( holdsAt(spinning(trolley2),n1)
| ~ happens(pull(agent2,trolley2),n0) ),
inference(paramod,[status(thm)],[c_188,c_1747]) ).
cnf(c_1639,plain,
holdsAt(spinning(trolley2),n1),
inference(resolve,[status(thm)],[c_731,c_1748]) ).
cnf(c_1652,negated_conjecture,
~ holdsAt(spinning(trolley1),n1),
inference(resolve,[status(thm)],[c_1639,c_1601]) ).
cnf(c_1689,plain,
initiates(pull(agent1,trolley1),spinning(trolley1),n0),
inference(xxres,[status(thm)],[c_1071]) ).
cnf(c_1749,plain,
( holdsAt(spinning(trolley1),plus(n0,n1))
| ~ happens(pull(agent1,trolley1),n0) ),
inference(resolve,[status(thm)],[c_1689,c_231]) ).
cnf(c_1750,plain,
( holdsAt(spinning(trolley1),n1)
| ~ happens(pull(agent1,trolley1),n0) ),
inference(paramod,[status(thm)],[c_188,c_1749]) ).
cnf(c_1751,plain,
holdsAt(spinning(trolley1),n1),
inference(resolve,[status(thm)],[c_736,c_1750]) ).
cnf(c_1690,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1652,c_1751]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR024+1.010 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n020.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 23:57:34 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.35 % Process 2820529 was started by sandbox on n020,
% 0.13/0.35 % Sat Sep 26 23:57:34 2026
% 0.13/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/0.38
% 0.13/0.38 % From the command line: assign(max_seconds, 300).
% 24.88/3.55
% 24.88/3.55 % given #500 (T,wt=9): 758 less(n1,A) | n1 = A | less_or_equal(A,n2). [resolve(746,c,177,b)].
% 24.88/3.55
% 24.88/3.55 % SZS status Theorem for theBenchmark
% 24.88/3.55
% 24.88/3.55 % Proof 1 at 3.03 (+ 0.12) seconds.
% 24.88/3.55 % Length of proof is 118.
% 24.88/3.55 % Level of proof is 17.
% 24.88/3.55 % Maximum clause weight is 40.000.
% 24.88/3.55 % Given clauses 906.
% 24.88/3.55
% 24.88/3.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------