%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR024+1.009 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:05:13 PM UTC 2026
% Result : Theorem 124.97s 17.20s
% Output : Proof 124.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 4
% Syntax : Number of formulae : 199 ( 57 unt; 0 def)
% Number of atoms : 646 ( 268 equ)
% Maximal formula atoms : 74 ( 3 avg)
% Number of connectives : 772 ( 325 ~; 313 |; 131 &)
% ( 2 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 42 ( 40 usr; 1 prp; 0-3 aty)
% Number of functors : 28 ( 28 usr; 20 con; 0-3 aty)
% Number of variables : 257 ( 4 sgn 28 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f47,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('/export/starexec/sandbox/benchmark/theBenchmark.p',happens_all_defn) ).
fof(f47_nnf,plain,
! [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) ) )
| 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) )
| ~ happens(Event,Time) ) ),
inference(nnf_transformation,[status(thm)],[f47]) ).
fof(f47_sk,plain,
! [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) ) )
| 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) )
| ~ happens(Event,Time) ) ),
inference(skolemisation,[status(esa)],[f47_nnf]) ).
cnf(c494,plain,
( X1 != n0
| X0 != pull(agent4,trolley4)
| ~ def121(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2525,plain,
( X0 != pull(agent4,trolley4)
| ~ def121(X0,n0) ),
inference(equality_resolution,[status(thm)],[c494]) ).
cnf(c566,plain,
( def144(X0,X1)
| happens(X0,X1)
| ~ def145(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(c570,plain,
( def145(X0,X1)
| ~ def146(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(c572,plain,
def146(X0,X1),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p893,plain,
def145(X0,X1),
inference(resolution,[status(thm)],[c570,c572]) ).
cnf(p1339,plain,
( def144(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[c566,p893]) ).
cnf(c563,plain,
( def142(X0,X1)
| ~ def144(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1340,plain,
( def142(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1339,c563]) ).
cnf(c557,plain,
( def140(X0,X1)
| ~ def142(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1342,plain,
( def140(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1340,c557]) ).
cnf(c551,plain,
( def138(X0,X1)
| ~ def140(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1346,plain,
( def138(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1342,c551]) ).
cnf(c545,plain,
( def136(X0,X1)
| ~ def138(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1348,plain,
( def136(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1346,c545]) ).
cnf(c539,plain,
( def134(X0,X1)
| ~ def136(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1352,plain,
( def134(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1348,c539]) ).
cnf(c533,plain,
( def132(X0,X1)
| ~ def134(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1354,plain,
( def132(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1352,c533]) ).
cnf(c527,plain,
( def130(X0,X1)
| ~ def132(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1356,plain,
( def130(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1354,c527]) ).
cnf(c521,plain,
( def128(X0,X1)
| ~ def130(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1358,plain,
( def128(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1356,c521]) ).
cnf(c515,plain,
( def126(X0,X1)
| ~ def128(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1361,plain,
( def126(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1358,c515]) ).
cnf(c509,plain,
( def124(X0,X1)
| ~ def126(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1363,plain,
( def124(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1361,c509]) ).
cnf(c503,plain,
( def122(X0,X1)
| ~ def124(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1368,plain,
( def122(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1363,c503]) ).
cnf(c498,plain,
( def121(X0,X1)
| ~ def122(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1371,plain,
( def121(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1368,c498]) ).
cnf(p4262,plain,
( happens(X0,n0)
| X0 != pull(agent4,trolley4) ),
inference(resolution,[status(thm)],[p2525,p1371]) ).
cnf(p6092,plain,
happens(pull(agent4,trolley4),n0),
inference(equality_resolution,[status(thm)],[p4262]) ).
fof(f8,axiom,
! [Event,Time,Fluent] :
( ( initiates(Event,Fluent,Time)
& happens(Event,Time) )
=> holdsAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',happens_holds) ).
fof(f8_nnf,plain,
! [Event,Time,Fluent] :
( holdsAt(Fluent,plus(Time,n1))
| ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [Event,Time,Fluent] :
( holdsAt(Fluent,plus(Time,n1))
| ~ initiates(Event,Fluent,Time)
| ~ happens(Event,Time) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c20,plain,
( holdsAt(X2,plus(X1,n1))
| ~ initiates(X0,X2,X1)
| ~ happens(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p6101,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent4,trolley4),X0,n0) ),
inference(resolution,[status(thm)],[p6092,c20]) ).
fof(f12,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('/export/starexec/sandbox/benchmark/theBenchmark.p',initiates_all_defn) ).
fof(f12_nnf,plain,
! [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) ) )
| 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) ) )
| ~ initiates(Event,Fluent,Time) ) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [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) ) )
| initiates(Event,Fluent,Time) )
& ( ( happens(push(sk8(Event,Fluent,Time),sk9(Event,Fluent,Time)),Time)
& Fluent = spinning(sk9(Event,Fluent,Time))
& Event = pull(sk8(Event,Fluent,Time),sk9(Event,Fluent,Time)) )
| ( ~ happens(push(sk8(Event,Fluent,Time),sk9(Event,Fluent,Time)),Time)
& Fluent = backwards(sk9(Event,Fluent,Time))
& Event = pull(sk8(Event,Fluent,Time),sk9(Event,Fluent,Time)) )
| ( ~ happens(pull(sk8(Event,Fluent,Time),sk9(Event,Fluent,Time)),Time)
& Fluent = forwards(sk9(Event,Fluent,Time))
& Event = push(sk8(Event,Fluent,Time),sk9(Event,Fluent,Time)) )
| ~ initiates(Event,Fluent,Time) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk8,sk9])],[f12_nnf]) ).
cnf(c54,plain,
( ~ happens(push(X3,X4),X2)
| X1 != spinning(X4)
| X0 != pull(X3,X4)
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p750,plain,
( ~ happens(push(X0,X1),X3)
| X2 != spinning(X1)
| initiates(pull(X0,X1),X2,X3) ),
inference(equality_resolution,[status(thm)],[c54]) ).
cnf(p3138,plain,
( ~ happens(push(X0,X1),X2)
| initiates(pull(X0,X1),spinning(X1),X2) ),
inference(equality_resolution,[status(thm)],[p750]) ).
cnf(c500,plain,
( X1 != n0
| X0 != push(agent4,trolley4)
| ~ def123(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2568,plain,
( X0 != n0
| ~ def123(push(agent4,trolley4),X0) ),
inference(equality_resolution,[status(thm)],[c500]) ).
cnf(p4312,plain,
~ def123(push(agent4,trolley4),n0),
inference(equality_resolution,[status(thm)],[p2568]) ).
cnf(c504,plain,
( def123(X0,X1)
| ~ def124(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1369,plain,
( def123(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1363,c504]) ).
cnf(p4326,plain,
happens(push(agent4,trolley4),n0),
inference(resolution,[status(thm)],[p4312,p1369]) ).
cnf(p34123,plain,
initiates(pull(agent4,trolley4),spinning(trolley4),n0),
inference(resolution,[status(thm)],[p3138,p4326]) ).
cnf(p49208,plain,
holdsAt(spinning(trolley4),n1),
inference(resolution,[status(thm)],[p6101,p34123]) ).
cnf(c482,plain,
( X1 != n0
| X0 != pull(agent3,trolley3)
| ~ def117(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2446,plain,
( X0 != n0
| ~ def117(pull(agent3,trolley3),X0) ),
inference(equality_resolution,[status(thm)],[c482]) ).
cnf(p4039,plain,
~ def117(pull(agent3,trolley3),n0),
inference(equality_resolution,[status(thm)],[p2446]) ).
cnf(c497,plain,
( def120(X0,X1)
| ~ def122(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1370,plain,
( def120(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1368,c497]) ).
cnf(c491,plain,
( def118(X0,X1)
| ~ def120(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1373,plain,
( def118(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1370,c491]) ).
cnf(c486,plain,
( def117(X0,X1)
| ~ def118(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1376,plain,
( def117(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1373,c486]) ).
cnf(p4053,plain,
happens(pull(agent3,trolley3),n0),
inference(resolution,[status(thm)],[p4039,p1376]) ).
cnf(p4066,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent3,trolley3),X0,n0) ),
inference(resolution,[status(thm)],[p4053,c20]) ).
cnf(c488,plain,
( X1 != n0
| X0 != push(agent3,trolley3)
| ~ def119(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2494,plain,
( X0 != n0
| ~ def119(push(agent3,trolley3),X0) ),
inference(equality_resolution,[status(thm)],[c488]) ).
cnf(p4149,plain,
~ def119(push(agent3,trolley3),n0),
inference(equality_resolution,[status(thm)],[p2494]) ).
cnf(c492,plain,
( def119(X0,X1)
| ~ def120(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1374,plain,
( def119(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1370,c492]) ).
cnf(p4163,plain,
happens(push(agent3,trolley3),n0),
inference(resolution,[status(thm)],[p4149,p1374]) ).
cnf(p34122,plain,
initiates(pull(agent3,trolley3),spinning(trolley3),n0),
inference(resolution,[status(thm)],[p3138,p4163]) ).
cnf(p48022,plain,
holdsAt(spinning(trolley3),n1),
inference(resolution,[status(thm)],[p4066,p34122]) ).
cnf(c470,plain,
( X1 != n0
| X0 != pull(agent2,trolley2)
| ~ def113(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2364,plain,
( X0 != n0
| ~ def113(pull(agent2,trolley2),X0) ),
inference(equality_resolution,[status(thm)],[c470]) ).
cnf(p3806,plain,
~ def113(pull(agent2,trolley2),n0),
inference(equality_resolution,[status(thm)],[p2364]) ).
cnf(c485,plain,
( def116(X0,X1)
| ~ def118(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1375,plain,
( def116(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1373,c485]) ).
cnf(c479,plain,
( def114(X0,X1)
| ~ def116(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1378,plain,
( def114(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1375,c479]) ).
cnf(c474,plain,
( def113(X0,X1)
| ~ def114(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1381,plain,
( def113(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1378,c474]) ).
cnf(p3820,plain,
happens(pull(agent2,trolley2),n0),
inference(resolution,[status(thm)],[p3806,p1381]) ).
cnf(p3833,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent2,trolley2),X0,n0) ),
inference(resolution,[status(thm)],[p3820,c20]) ).
cnf(c476,plain,
( X1 != n0
| X0 != push(agent2,trolley2)
| ~ def115(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2412,plain,
( X0 != n0
| ~ def115(push(agent2,trolley2),X0) ),
inference(equality_resolution,[status(thm)],[c476]) ).
cnf(p3919,plain,
~ def115(push(agent2,trolley2),n0),
inference(equality_resolution,[status(thm)],[p2412]) ).
cnf(c480,plain,
( def115(X0,X1)
| ~ def116(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1379,plain,
( def115(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1375,c480]) ).
cnf(p3933,plain,
happens(push(agent2,trolley2),n0),
inference(resolution,[status(thm)],[p3919,p1379]) ).
cnf(p34121,plain,
initiates(pull(agent2,trolley2),spinning(trolley2),n0),
inference(resolution,[status(thm)],[p3138,p3933]) ).
cnf(p44686,plain,
holdsAt(spinning(trolley2),n1),
inference(resolution,[status(thm)],[p3833,p34121]) ).
cnf(c461,plain,
( X1 != n0
| X0 != pull(agent1,trolley1)
| ~ def110(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2253,plain,
( X0 != n0
| ~ def110(pull(agent1,trolley1),X0) ),
inference(equality_resolution,[status(thm)],[c461]) ).
cnf(p3587,plain,
~ def110(pull(agent1,trolley1),n0),
inference(equality_resolution,[status(thm)],[p2253]) ).
cnf(c473,plain,
( def112(X0,X1)
| ~ def114(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1380,plain,
( def112(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1378,c473]) ).
cnf(c467,plain,
( def110(X0,X1)
| ~ def112(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1382,plain,
( def110(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1380,c467]) ).
cnf(p3619,plain,
happens(pull(agent1,trolley1),n0),
inference(resolution,[status(thm)],[p3587,p1382]) ).
cnf(p3632,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent1,trolley1),X0,n0) ),
inference(resolution,[status(thm)],[p3619,c20]) ).
cnf(c464,plain,
( X1 != n0
| X0 != push(agent1,trolley1)
| ~ def111(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2314,plain,
( X0 != n0
| ~ def111(push(agent1,trolley1),X0) ),
inference(equality_resolution,[status(thm)],[c464]) ).
cnf(p3703,plain,
~ def111(push(agent1,trolley1),n0),
inference(equality_resolution,[status(thm)],[p2314]) ).
cnf(c468,plain,
( def111(X0,X1)
| ~ def112(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1383,plain,
( def111(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1380,c468]) ).
cnf(p3717,plain,
happens(push(agent1,trolley1),n0),
inference(resolution,[status(thm)],[p3703,p1383]) ).
cnf(p34120,plain,
initiates(pull(agent1,trolley1),spinning(trolley1),n0),
inference(resolution,[status(thm)],[p3138,p3717]) ).
cnf(p42491,plain,
holdsAt(spinning(trolley1),n1),
inference(resolution,[status(thm)],[p3632,p34120]) ).
fof(f57,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('/export/starexec/sandbox/benchmark/theBenchmark.p',spinning_3) ).
fof(f57_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(negated_conjecture,[status(cth)],[f57]) ).
fof(f57_nnf,plain,
( ~ 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(nnf_transformation,[status(thm)],[f57_neg]) ).
fof(f57_sk,plain,
( ~ 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(skolemisation,[status(esa)],[f57_nnf]) ).
cnf(c679,plain,
( ~ 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(cnf_transformation,[status(esa)],[f57_sk]) ).
cnf(p42500,plain,
( ~ 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(resolution,[status(thm)],[p42491,c679]) ).
cnf(p44698,plain,
( ~ 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(resolution,[status(thm)],[p44686,p42500]) ).
cnf(p48033,plain,
( ~ 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(resolution,[status(thm)],[p48022,p44698]) ).
cnf(p49213,plain,
( ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley5),n1) ),
inference(resolution,[status(thm)],[p49208,p48033]) ).
cnf(c506,plain,
( X1 != n0
| X0 != pull(agent5,trolley5)
| ~ def125(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2598,plain,
( X0 != n0
| ~ def125(pull(agent5,trolley5),X0) ),
inference(equality_resolution,[status(thm)],[c506]) ).
cnf(p4410,plain,
~ def125(pull(agent5,trolley5),n0),
inference(equality_resolution,[status(thm)],[p2598]) ).
cnf(c510,plain,
( def125(X0,X1)
| ~ def126(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1364,plain,
( def125(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1361,c510]) ).
cnf(p4424,plain,
happens(pull(agent5,trolley5),n0),
inference(resolution,[status(thm)],[p4410,p1364]) ).
cnf(p4437,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent5,trolley5),X0,n0) ),
inference(resolution,[status(thm)],[p4424,c20]) ).
cnf(c512,plain,
( X1 != n0
| X0 != push(agent5,trolley5)
| ~ def127(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2642,plain,
( X0 != n0
| ~ def127(push(agent5,trolley5),X0) ),
inference(equality_resolution,[status(thm)],[c512]) ).
cnf(p4515,plain,
~ def127(push(agent5,trolley5),n0),
inference(equality_resolution,[status(thm)],[p2642]) ).
cnf(c516,plain,
( def127(X0,X1)
| ~ def128(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1362,plain,
( def127(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1358,c516]) ).
cnf(p4529,plain,
happens(push(agent5,trolley5),n0),
inference(resolution,[status(thm)],[p4515,p1362]) ).
cnf(p34124,plain,
initiates(pull(agent5,trolley5),spinning(trolley5),n0),
inference(resolution,[status(thm)],[p3138,p4529]) ).
cnf(p49124,plain,
holdsAt(spinning(trolley5),n1),
inference(resolution,[status(thm)],[p4437,p34124]) ).
cnf(p49214,plain,
( ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1) ),
inference(resolution,[status(thm)],[p49213,p49124]) ).
cnf(c518,plain,
( X1 != n0
| X0 != pull(agent6,trolley6)
| ~ def129(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2672,plain,
( X0 != n0
| ~ def129(pull(agent6,trolley6),X0) ),
inference(equality_resolution,[status(thm)],[c518]) ).
cnf(p4613,plain,
~ def129(pull(agent6,trolley6),n0),
inference(equality_resolution,[status(thm)],[p2672]) ).
cnf(c522,plain,
( def129(X0,X1)
| ~ def130(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1359,plain,
( def129(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1356,c522]) ).
cnf(p4627,plain,
happens(pull(agent6,trolley6),n0),
inference(resolution,[status(thm)],[p4613,p1359]) ).
cnf(p4640,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent6,trolley6),X0,n0) ),
inference(resolution,[status(thm)],[p4627,c20]) ).
cnf(c524,plain,
( X1 != n0
| X0 != push(agent6,trolley6)
| ~ def131(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2719,plain,
( X0 != n0
| ~ def131(push(agent6,trolley6),X0) ),
inference(equality_resolution,[status(thm)],[c524]) ).
cnf(p4715,plain,
~ def131(push(agent6,trolley6),n0),
inference(equality_resolution,[status(thm)],[p2719]) ).
cnf(c528,plain,
( def131(X0,X1)
| ~ def132(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1357,plain,
( def131(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1354,c528]) ).
cnf(p4739,plain,
happens(push(agent6,trolley6),n0),
inference(resolution,[status(thm)],[p4715,p1357]) ).
cnf(p34125,plain,
initiates(pull(agent6,trolley6),spinning(trolley6),n0),
inference(resolution,[status(thm)],[p3138,p4739]) ).
cnf(p49143,plain,
holdsAt(spinning(trolley6),n1),
inference(resolution,[status(thm)],[p4640,p34125]) ).
cnf(p49216,plain,
( ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1) ),
inference(resolution,[status(thm)],[p49214,p49143]) ).
cnf(c530,plain,
( X1 != n0
| X0 != pull(agent7,trolley7)
| ~ def133(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2753,plain,
( X0 != n0
| ~ def133(pull(agent7,trolley7),X0) ),
inference(equality_resolution,[status(thm)],[c530]) ).
cnf(p4812,plain,
~ def133(pull(agent7,trolley7),n0),
inference(equality_resolution,[status(thm)],[p2753]) ).
cnf(c534,plain,
( def133(X0,X1)
| ~ def134(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1355,plain,
( def133(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1352,c534]) ).
cnf(p4826,plain,
happens(pull(agent7,trolley7),n0),
inference(resolution,[status(thm)],[p4812,p1355]) ).
cnf(p4850,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent7,trolley7),X0,n0) ),
inference(resolution,[status(thm)],[p4826,c20]) ).
cnf(c536,plain,
( X1 != n0
| X0 != push(agent7,trolley7)
| ~ def135(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2801,plain,
( X0 != n0
| ~ def135(push(agent7,trolley7),X0) ),
inference(equality_resolution,[status(thm)],[c536]) ).
cnf(p4923,plain,
~ def135(push(agent7,trolley7),n0),
inference(equality_resolution,[status(thm)],[p2801]) ).
cnf(c540,plain,
( def135(X0,X1)
| ~ def136(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1353,plain,
( def135(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1348,c540]) ).
cnf(p4937,plain,
happens(push(agent7,trolley7),n0),
inference(resolution,[status(thm)],[p4923,p1353]) ).
cnf(p34126,plain,
initiates(pull(agent7,trolley7),spinning(trolley7),n0),
inference(resolution,[status(thm)],[p3138,p4937]) ).
cnf(p49160,plain,
holdsAt(spinning(trolley7),n1),
inference(resolution,[status(thm)],[p4850,p34126]) ).
cnf(p49217,plain,
( ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1) ),
inference(resolution,[status(thm)],[p49216,p49160]) ).
cnf(c542,plain,
( X1 != n0
| X0 != pull(agent8,trolley8)
| ~ def137(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2835,plain,
( X0 != n0
| ~ def137(pull(agent8,trolley8),X0) ),
inference(equality_resolution,[status(thm)],[c542]) ).
cnf(p5007,plain,
~ def137(pull(agent8,trolley8),n0),
inference(equality_resolution,[status(thm)],[p2835]) ).
cnf(c546,plain,
( def137(X0,X1)
| ~ def138(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1349,plain,
( def137(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1346,c546]) ).
cnf(p5030,plain,
happens(pull(agent8,trolley8),n0),
inference(resolution,[status(thm)],[p5007,p1349]) ).
cnf(p5039,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent8,trolley8),X0,n0) ),
inference(resolution,[status(thm)],[p5030,c20]) ).
cnf(c548,plain,
( X1 != n0
| X0 != push(agent8,trolley8)
| ~ def139(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2870,plain,
( X0 != n0
| ~ def139(push(agent8,trolley8),X0) ),
inference(equality_resolution,[status(thm)],[c548]) ).
cnf(p5102,plain,
~ def139(push(agent8,trolley8),n0),
inference(equality_resolution,[status(thm)],[p2870]) ).
cnf(c552,plain,
( def139(X0,X1)
| ~ def140(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1347,plain,
( def139(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1342,c552]) ).
cnf(p5107,plain,
happens(push(agent8,trolley8),n0),
inference(resolution,[status(thm)],[p5102,p1347]) ).
cnf(p34127,plain,
initiates(pull(agent8,trolley8),spinning(trolley8),n0),
inference(resolution,[status(thm)],[p3138,p5107]) ).
cnf(p49175,plain,
holdsAt(spinning(trolley8),n1),
inference(resolution,[status(thm)],[p5039,p34127]) ).
cnf(p49218,plain,
~ holdsAt(spinning(trolley9),n1),
inference(resolution,[status(thm)],[p49217,p49175]) ).
cnf(c554,plain,
( X1 != n0
| X0 != pull(agent9,trolley9)
| ~ def141(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2882,plain,
( X0 != n0
| ~ def141(pull(agent9,trolley9),X0) ),
inference(equality_resolution,[status(thm)],[c554]) ).
cnf(p5148,plain,
~ def141(pull(agent9,trolley9),n0),
inference(equality_resolution,[status(thm)],[p2882]) ).
cnf(c558,plain,
( def141(X0,X1)
| ~ def142(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1343,plain,
( def141(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1340,c558]) ).
cnf(p5153,plain,
happens(pull(agent9,trolley9),n0),
inference(resolution,[status(thm)],[p5148,p1343]) ).
cnf(p5157,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent9,trolley9),X0,n0) ),
inference(resolution,[status(thm)],[p5153,c20]) ).
cnf(c560,plain,
( X1 != n0
| X0 != push(agent9,trolley9)
| ~ def143(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p2907,plain,
( X0 != n0
| ~ def143(push(agent9,trolley9),X0) ),
inference(equality_resolution,[status(thm)],[c560]) ).
cnf(p5207,plain,
~ def143(push(agent9,trolley9),n0),
inference(equality_resolution,[status(thm)],[p2907]) ).
cnf(c564,plain,
( def143(X0,X1)
| ~ def144(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146])],[f47_sk]) ).
cnf(p1341,plain,
( def143(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1339,c564]) ).
cnf(p5212,plain,
happens(push(agent9,trolley9),n0),
inference(resolution,[status(thm)],[p5207,p1341]) ).
cnf(p34128,plain,
initiates(pull(agent9,trolley9),spinning(trolley9),n0),
inference(resolution,[status(thm)],[p3138,p5212]) ).
cnf(p49188,plain,
holdsAt(spinning(trolley9),n1),
inference(resolution,[status(thm)],[p5157,p34128]) ).
cnf(p49219,plain,
$false,
inference(resolution,[status(thm)],[p49218,p49188]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR024+1.009 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n005.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 25 08:07:47 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 124.97/17.20 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 124.97/17.20 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------