%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : CSR024+1.009 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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:33 AM UTC 2026
% Result : Theorem 11.43s 1.95s
% Output : CNFRefutation 11.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 6
% Syntax : Number of formulae : 165 ( 78 unt; 0 def)
% Number of atoms : 368 ( 147 equ)
% Maximal formula atoms : 37 ( 2 avg)
% Number of connectives : 355 ( 152 ~; 159 |; 41 &)
% ( 2 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 20 con; 0-2 aty)
% Number of variables : 99 ( 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(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(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(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_152,plain,
( holdsAt(C,plus(B,n1))
| ~ initiates(A,C,B)
| ~ happens(A,B) ),
inference(clausify,[status(thm)],[happens_holds]) ).
cnf(c_170,plain,
( ~ happens(push(D,E),C)
| spinning(E) != B
| pull(D,E) != A
| initiates(A,B,C) ),
inference(clausify,[status(thm)],[initiates_all_defn]) ).
fof(plus0_0,axiom,
plus(n0,n0) = n0,
file('theBenchmark.p',plus0_0) ).
cnf(c_194,plain,
plus(n0,n0) = n0,
inference(clausify,[status(thm)],[plus0_0]) ).
fof(plus0_1,axiom,
plus(n0,n1) = n1,
file('theBenchmark.p',plus0_1) ).
cnf(c_195,plain,
plus(n0,n1) = n1,
inference(clausify,[status(thm)],[plus0_1]) ).
cnf(c_250,plain,
( n0 != B
| pull(agent1,trolley1) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_251,plain,
( n0 != B
| push(agent1,trolley1) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_252,plain,
( n0 != B
| pull(agent2,trolley2) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_253,plain,
( n0 != B
| push(agent2,trolley2) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_254,plain,
( n0 != B
| pull(agent3,trolley3) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_255,plain,
( n0 != B
| push(agent3,trolley3) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_256,plain,
( n0 != B
| pull(agent4,trolley4) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_257,plain,
( n0 != B
| push(agent4,trolley4) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_258,plain,
( n0 != B
| pull(agent5,trolley5) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_259,plain,
( n0 != B
| push(agent5,trolley5) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_260,plain,
( n0 != B
| pull(agent6,trolley6) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_261,plain,
( n0 != B
| push(agent6,trolley6) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_262,plain,
( n0 != B
| pull(agent7,trolley7) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_263,plain,
( n0 != B
| push(agent7,trolley7) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_264,plain,
( n0 != B
| pull(agent8,trolley8) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_265,plain,
( n0 != B
| push(agent8,trolley8) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_266,plain,
( n0 != B
| pull(agent9,trolley9) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_267,plain,
( n0 != B
| push(agent9,trolley9) != A
| happens(A,B) ),
inference(clausify,[status(thm)],[happens_all_defn]) ).
cnf(c_379,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(clausify,[status(thm)],[spinning_3_neg]) ).
cnf(c_429,plain,
( n0 != A
| happens(pull(agent1,trolley1),A) ),
inference(xxres,[status(thm)],[c_250]) ).
cnf(c_431,plain,
( n0 != A
| happens(push(agent1,trolley1),A) ),
inference(xxres,[status(thm)],[c_251]) ).
cnf(c_433,plain,
( n0 != A
| happens(pull(agent2,trolley2),A) ),
inference(xxres,[status(thm)],[c_252]) ).
cnf(c_435,plain,
( n0 != A
| happens(push(agent2,trolley2),A) ),
inference(xxres,[status(thm)],[c_253]) ).
cnf(c_437,plain,
( n0 != A
| happens(pull(agent3,trolley3),A) ),
inference(xxres,[status(thm)],[c_254]) ).
cnf(c_439,plain,
( n0 != A
| happens(push(agent3,trolley3),A) ),
inference(xxres,[status(thm)],[c_255]) ).
cnf(c_441,plain,
( n0 != A
| happens(pull(agent4,trolley4),A) ),
inference(xxres,[status(thm)],[c_256]) ).
cnf(c_443,plain,
( n0 != A
| happens(push(agent4,trolley4),A) ),
inference(xxres,[status(thm)],[c_257]) ).
cnf(c_445,plain,
( n0 != A
| happens(pull(agent5,trolley5),A) ),
inference(xxres,[status(thm)],[c_258]) ).
cnf(c_447,plain,
( n0 != A
| happens(push(agent5,trolley5),A) ),
inference(xxres,[status(thm)],[c_259]) ).
cnf(c_449,plain,
( n0 != A
| happens(pull(agent6,trolley6),A) ),
inference(xxres,[status(thm)],[c_260]) ).
cnf(c_451,plain,
( n0 != A
| happens(push(agent6,trolley6),A) ),
inference(xxres,[status(thm)],[c_261]) ).
cnf(c_453,plain,
( n0 != A
| happens(pull(agent7,trolley7),A) ),
inference(xxres,[status(thm)],[c_262]) ).
cnf(c_455,plain,
( n0 != A
| happens(push(agent7,trolley7),A) ),
inference(xxres,[status(thm)],[c_263]) ).
cnf(c_457,plain,
( n0 != A
| happens(pull(agent8,trolley8),A) ),
inference(xxres,[status(thm)],[c_264]) ).
cnf(c_459,plain,
( n0 != A
| happens(push(agent8,trolley8),A) ),
inference(xxres,[status(thm)],[c_265]) ).
cnf(c_461,plain,
( n0 != A
| happens(pull(agent9,trolley9),A) ),
inference(xxres,[status(thm)],[c_266]) ).
cnf(c_463,plain,
( n0 != A
| happens(push(agent9,trolley9),A) ),
inference(xxres,[status(thm)],[c_267]) ).
cnf(c_2056,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2057,plain,
happens(pull(agent1,trolley1),plus(n0,n0)),
inference(resolve,[status(thm)],[c_429,c_2056]) ).
cnf(c_666,plain,
happens(pull(agent1,trolley1),n0),
inference(paramod,[status(thm)],[c_194,c_2057]) ).
cnf(c_2058,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2059,plain,
happens(push(agent1,trolley1),plus(n0,n0)),
inference(resolve,[status(thm)],[c_431,c_2058]) ).
cnf(c_667,plain,
happens(push(agent1,trolley1),n0),
inference(paramod,[status(thm)],[c_194,c_2059]) ).
cnf(c_670,plain,
( spinning(trolley1) != B
| pull(agent1,trolley1) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_667,c_170]) ).
cnf(c_2060,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2061,plain,
happens(pull(agent2,trolley2),plus(n0,n0)),
inference(resolve,[status(thm)],[c_433,c_2060]) ).
cnf(c_671,plain,
happens(pull(agent2,trolley2),n0),
inference(paramod,[status(thm)],[c_194,c_2061]) ).
cnf(c_2062,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2063,plain,
happens(push(agent2,trolley2),plus(n0,n0)),
inference(resolve,[status(thm)],[c_435,c_2062]) ).
cnf(c_672,plain,
happens(push(agent2,trolley2),n0),
inference(paramod,[status(thm)],[c_194,c_2063]) ).
cnf(c_675,plain,
( spinning(trolley2) != B
| pull(agent2,trolley2) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_672,c_170]) ).
cnf(c_2064,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2065,plain,
happens(pull(agent3,trolley3),plus(n0,n0)),
inference(resolve,[status(thm)],[c_437,c_2064]) ).
cnf(c_676,plain,
happens(pull(agent3,trolley3),n0),
inference(paramod,[status(thm)],[c_194,c_2065]) ).
cnf(c_2066,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2067,plain,
happens(push(agent3,trolley3),plus(n0,n0)),
inference(resolve,[status(thm)],[c_439,c_2066]) ).
cnf(c_677,plain,
happens(push(agent3,trolley3),n0),
inference(paramod,[status(thm)],[c_194,c_2067]) ).
cnf(c_680,plain,
( spinning(trolley3) != B
| pull(agent3,trolley3) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_677,c_170]) ).
cnf(c_2068,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2069,plain,
happens(pull(agent4,trolley4),plus(n0,n0)),
inference(resolve,[status(thm)],[c_441,c_2068]) ).
cnf(c_681,plain,
happens(pull(agent4,trolley4),n0),
inference(paramod,[status(thm)],[c_194,c_2069]) ).
cnf(c_2070,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2071,plain,
happens(push(agent4,trolley4),plus(n0,n0)),
inference(resolve,[status(thm)],[c_443,c_2070]) ).
cnf(c_682,plain,
happens(push(agent4,trolley4),n0),
inference(paramod,[status(thm)],[c_194,c_2071]) ).
cnf(c_685,plain,
( spinning(trolley4) != B
| pull(agent4,trolley4) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_682,c_170]) ).
cnf(c_2072,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2073,plain,
happens(pull(agent5,trolley5),plus(n0,n0)),
inference(resolve,[status(thm)],[c_445,c_2072]) ).
cnf(c_686,plain,
happens(pull(agent5,trolley5),n0),
inference(paramod,[status(thm)],[c_194,c_2073]) ).
cnf(c_2074,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2075,plain,
happens(push(agent5,trolley5),plus(n0,n0)),
inference(resolve,[status(thm)],[c_447,c_2074]) ).
cnf(c_687,plain,
happens(push(agent5,trolley5),n0),
inference(paramod,[status(thm)],[c_194,c_2075]) ).
cnf(c_690,plain,
( spinning(trolley5) != B
| pull(agent5,trolley5) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_687,c_170]) ).
cnf(c_2076,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2077,plain,
happens(pull(agent6,trolley6),plus(n0,n0)),
inference(resolve,[status(thm)],[c_449,c_2076]) ).
cnf(c_691,plain,
happens(pull(agent6,trolley6),n0),
inference(paramod,[status(thm)],[c_194,c_2077]) ).
cnf(c_2078,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2079,plain,
happens(push(agent6,trolley6),plus(n0,n0)),
inference(resolve,[status(thm)],[c_451,c_2078]) ).
cnf(c_692,plain,
happens(push(agent6,trolley6),n0),
inference(paramod,[status(thm)],[c_194,c_2079]) ).
cnf(c_695,plain,
( spinning(trolley6) != B
| pull(agent6,trolley6) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_692,c_170]) ).
cnf(c_2080,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2081,plain,
happens(pull(agent7,trolley7),plus(n0,n0)),
inference(resolve,[status(thm)],[c_453,c_2080]) ).
cnf(c_696,plain,
happens(pull(agent7,trolley7),n0),
inference(paramod,[status(thm)],[c_194,c_2081]) ).
cnf(c_2082,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2083,plain,
happens(push(agent7,trolley7),plus(n0,n0)),
inference(resolve,[status(thm)],[c_455,c_2082]) ).
cnf(c_697,plain,
happens(push(agent7,trolley7),n0),
inference(paramod,[status(thm)],[c_194,c_2083]) ).
cnf(c_700,plain,
( spinning(trolley7) != B
| pull(agent7,trolley7) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_697,c_170]) ).
cnf(c_2084,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2085,plain,
happens(pull(agent8,trolley8),plus(n0,n0)),
inference(resolve,[status(thm)],[c_457,c_2084]) ).
cnf(c_701,plain,
happens(pull(agent8,trolley8),n0),
inference(paramod,[status(thm)],[c_194,c_2085]) ).
cnf(c_2086,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2087,plain,
happens(push(agent8,trolley8),plus(n0,n0)),
inference(resolve,[status(thm)],[c_459,c_2086]) ).
cnf(c_702,plain,
happens(push(agent8,trolley8),n0),
inference(paramod,[status(thm)],[c_194,c_2087]) ).
cnf(c_705,plain,
( spinning(trolley8) != B
| pull(agent8,trolley8) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_702,c_170]) ).
cnf(c_2088,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2089,plain,
happens(pull(agent9,trolley9),plus(n0,n0)),
inference(resolve,[status(thm)],[c_461,c_2088]) ).
cnf(c_706,plain,
happens(pull(agent9,trolley9),n0),
inference(paramod,[status(thm)],[c_194,c_2089]) ).
cnf(c_2090,plain,
n0 = plus(n0,n0),
inference(copy,[status(thm)],[c_194]) ).
cnf(c_2091,plain,
happens(push(agent9,trolley9),plus(n0,n0)),
inference(resolve,[status(thm)],[c_463,c_2090]) ).
cnf(c_707,plain,
happens(push(agent9,trolley9),n0),
inference(paramod,[status(thm)],[c_194,c_2091]) ).
cnf(c_710,plain,
( spinning(trolley9) != B
| pull(agent9,trolley9) != A
| initiates(A,B,n0) ),
inference(resolve,[status(thm)],[c_707,c_170]) ).
cnf(c_1007,plain,
( spinning(trolley1) != A
| initiates(pull(agent1,trolley1),A,n0) ),
inference(xxres,[status(thm)],[c_670]) ).
cnf(c_1063,plain,
( spinning(trolley2) != A
| initiates(pull(agent2,trolley2),A,n0) ),
inference(xxres,[status(thm)],[c_675]) ).
cnf(c_1073,plain,
( spinning(trolley3) != A
| initiates(pull(agent3,trolley3),A,n0) ),
inference(xxres,[status(thm)],[c_680]) ).
cnf(c_1081,plain,
( spinning(trolley4) != A
| initiates(pull(agent4,trolley4),A,n0) ),
inference(xxres,[status(thm)],[c_685]) ).
cnf(c_1132,plain,
( spinning(trolley5) != A
| initiates(pull(agent5,trolley5),A,n0) ),
inference(xxres,[status(thm)],[c_690]) ).
cnf(c_1140,plain,
( spinning(trolley6) != A
| initiates(pull(agent6,trolley6),A,n0) ),
inference(xxres,[status(thm)],[c_695]) ).
cnf(c_1180,plain,
( spinning(trolley7) != A
| initiates(pull(agent7,trolley7),A,n0) ),
inference(xxres,[status(thm)],[c_700]) ).
cnf(c_1187,plain,
( spinning(trolley8) != A
| initiates(pull(agent8,trolley8),A,n0) ),
inference(xxres,[status(thm)],[c_705]) ).
cnf(c_1216,plain,
( spinning(trolley9) != A
| initiates(pull(agent9,trolley9),A,n0) ),
inference(xxres,[status(thm)],[c_710]) ).
cnf(c_1274,plain,
initiates(pull(agent1,trolley1),spinning(trolley1),n0),
inference(xxres,[status(thm)],[c_1007]) ).
cnf(c_2092,plain,
( holdsAt(spinning(trolley1),plus(n0,n1))
| ~ happens(pull(agent1,trolley1),n0) ),
inference(resolve,[status(thm)],[c_1274,c_152]) ).
cnf(c_2093,plain,
( holdsAt(spinning(trolley1),n1)
| ~ happens(pull(agent1,trolley1),n0) ),
inference(paramod,[status(thm)],[c_195,c_2092]) ).
cnf(c_1299,plain,
holdsAt(spinning(trolley1),n1),
inference(resolve,[status(thm)],[c_666,c_2093]) ).
cnf(c_1300,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) ),
inference(resolve,[status(thm)],[c_1299,c_379]) ).
cnf(c_1365,plain,
initiates(pull(agent2,trolley2),spinning(trolley2),n0),
inference(xxres,[status(thm)],[c_1063]) ).
cnf(c_2094,plain,
( holdsAt(spinning(trolley2),plus(n0,n1))
| ~ happens(pull(agent2,trolley2),n0) ),
inference(resolve,[status(thm)],[c_1365,c_152]) ).
cnf(c_2095,plain,
( holdsAt(spinning(trolley2),n1)
| ~ happens(pull(agent2,trolley2),n0) ),
inference(paramod,[status(thm)],[c_195,c_2094]) ).
cnf(c_1390,plain,
holdsAt(spinning(trolley2),n1),
inference(resolve,[status(thm)],[c_671,c_2095]) ).
cnf(c_1391,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) ),
inference(resolve,[status(thm)],[c_1390,c_1300]) ).
cnf(c_1461,plain,
initiates(pull(agent3,trolley3),spinning(trolley3),n0),
inference(xxres,[status(thm)],[c_1073]) ).
cnf(c_2096,plain,
( holdsAt(spinning(trolley3),plus(n0,n1))
| ~ happens(pull(agent3,trolley3),n0) ),
inference(resolve,[status(thm)],[c_1461,c_152]) ).
cnf(c_2097,plain,
( holdsAt(spinning(trolley3),n1)
| ~ happens(pull(agent3,trolley3),n0) ),
inference(paramod,[status(thm)],[c_195,c_2096]) ).
cnf(c_1486,plain,
holdsAt(spinning(trolley3),n1),
inference(resolve,[status(thm)],[c_676,c_2097]) ).
cnf(c_1487,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) ),
inference(resolve,[status(thm)],[c_1486,c_1391]) ).
cnf(c_1557,plain,
initiates(pull(agent4,trolley4),spinning(trolley4),n0),
inference(xxres,[status(thm)],[c_1081]) ).
cnf(c_2098,plain,
( holdsAt(spinning(trolley4),plus(n0,n1))
| ~ happens(pull(agent4,trolley4),n0) ),
inference(resolve,[status(thm)],[c_1557,c_152]) ).
cnf(c_2099,plain,
( holdsAt(spinning(trolley4),n1)
| ~ happens(pull(agent4,trolley4),n0) ),
inference(paramod,[status(thm)],[c_195,c_2098]) ).
cnf(c_1582,plain,
holdsAt(spinning(trolley4),n1),
inference(resolve,[status(thm)],[c_681,c_2099]) ).
cnf(c_1583,negated_conjecture,
( ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley5),n1) ),
inference(resolve,[status(thm)],[c_1582,c_1487]) ).
cnf(c_1650,plain,
initiates(pull(agent5,trolley5),spinning(trolley5),n0),
inference(xxres,[status(thm)],[c_1132]) ).
cnf(c_2100,plain,
( holdsAt(spinning(trolley5),plus(n0,n1))
| ~ happens(pull(agent5,trolley5),n0) ),
inference(resolve,[status(thm)],[c_1650,c_152]) ).
cnf(c_2101,plain,
( holdsAt(spinning(trolley5),n1)
| ~ happens(pull(agent5,trolley5),n0) ),
inference(paramod,[status(thm)],[c_195,c_2100]) ).
cnf(c_1675,plain,
holdsAt(spinning(trolley5),n1),
inference(resolve,[status(thm)],[c_686,c_2101]) ).
cnf(c_1676,negated_conjecture,
( ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1) ),
inference(resolve,[status(thm)],[c_1675,c_1583]) ).
cnf(c_1741,plain,
initiates(pull(agent6,trolley6),spinning(trolley6),n0),
inference(xxres,[status(thm)],[c_1140]) ).
cnf(c_2102,plain,
( holdsAt(spinning(trolley6),plus(n0,n1))
| ~ happens(pull(agent6,trolley6),n0) ),
inference(resolve,[status(thm)],[c_1741,c_152]) ).
cnf(c_2103,plain,
( holdsAt(spinning(trolley6),n1)
| ~ happens(pull(agent6,trolley6),n0) ),
inference(paramod,[status(thm)],[c_195,c_2102]) ).
cnf(c_1766,plain,
holdsAt(spinning(trolley6),n1),
inference(resolve,[status(thm)],[c_691,c_2103]) ).
cnf(c_1767,negated_conjecture,
( ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1) ),
inference(resolve,[status(thm)],[c_1766,c_1676]) ).
cnf(c_1837,plain,
initiates(pull(agent7,trolley7),spinning(trolley7),n0),
inference(xxres,[status(thm)],[c_1180]) ).
cnf(c_2104,plain,
( holdsAt(spinning(trolley7),plus(n0,n1))
| ~ happens(pull(agent7,trolley7),n0) ),
inference(resolve,[status(thm)],[c_1837,c_152]) ).
cnf(c_2105,plain,
( holdsAt(spinning(trolley7),n1)
| ~ happens(pull(agent7,trolley7),n0) ),
inference(paramod,[status(thm)],[c_195,c_2104]) ).
cnf(c_1862,plain,
holdsAt(spinning(trolley7),n1),
inference(resolve,[status(thm)],[c_696,c_2105]) ).
cnf(c_1863,negated_conjecture,
( ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1) ),
inference(resolve,[status(thm)],[c_1862,c_1767]) ).
cnf(c_1933,plain,
initiates(pull(agent8,trolley8),spinning(trolley8),n0),
inference(xxres,[status(thm)],[c_1187]) ).
cnf(c_2106,plain,
( holdsAt(spinning(trolley8),plus(n0,n1))
| ~ happens(pull(agent8,trolley8),n0) ),
inference(resolve,[status(thm)],[c_1933,c_152]) ).
cnf(c_2107,plain,
( holdsAt(spinning(trolley8),n1)
| ~ happens(pull(agent8,trolley8),n0) ),
inference(paramod,[status(thm)],[c_195,c_2106]) ).
cnf(c_1958,plain,
holdsAt(spinning(trolley8),n1),
inference(resolve,[status(thm)],[c_701,c_2107]) ).
cnf(c_1959,negated_conjecture,
~ holdsAt(spinning(trolley9),n1),
inference(resolve,[status(thm)],[c_1958,c_1863]) ).
cnf(c_2030,plain,
initiates(pull(agent9,trolley9),spinning(trolley9),n0),
inference(xxres,[status(thm)],[c_1216]) ).
cnf(c_2108,plain,
( holdsAt(spinning(trolley9),plus(n0,n1))
| ~ happens(pull(agent9,trolley9),n0) ),
inference(resolve,[status(thm)],[c_2030,c_152]) ).
cnf(c_2109,plain,
( holdsAt(spinning(trolley9),n1)
| ~ happens(pull(agent9,trolley9),n0) ),
inference(paramod,[status(thm)],[c_195,c_2108]) ).
cnf(c_2110,plain,
holdsAt(spinning(trolley9),n1),
inference(resolve,[status(thm)],[c_706,c_2109]) ).
cnf(c_2055,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1959,c_2110]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR024+1.009 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.38 % Computer : n018.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sat Sep 26 23:58:53 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.39 % Process 1731749 was started by sandbox2 on n018,
% 0.10/0.39 % Sat Sep 26 23:58:53 2026
% 0.10/0.39 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.41
% 0.10/0.41 % From the command line: assign(max_seconds, 300).
% 11.43/1.95
% 11.43/1.95 % given #500 (T,wt=9): 716 less(n8,A) | n8 = A | -less(n9,A). [resolve(658,c,227,b)].
% 11.43/1.95
% 11.43/1.95 % SZS status Theorem for theBenchmark
% 11.43/1.95
% 11.43/1.95 % Proof 1 at 1.10 (+ 0.13) seconds.
% 11.43/1.95 % Length of proof is 107.
% 11.43/1.95 % Level of proof is 16.
% 11.43/1.95 % Maximum clause weight is 36.000.
% 11.43/1.95 % Given clauses 910.
% 11.43/1.95
% 11.43/1.95 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------