%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR024+1.010 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n001.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 117.50s 16.46s
% Output : Proof 117.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 4
% Syntax : Number of formulae : 219 ( 64 unt; 0 def)
% Number of atoms : 713 ( 293 equ)
% Maximal formula atoms : 82 ( 3 avg)
% Number of connectives : 856 ( 362 ~; 348 |; 143 &)
% ( 2 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 46 ( 44 usr; 1 prp; 0-3 aty)
% Number of functors : 30 ( 30 usr; 22 con; 0-3 aty)
% Number of variables : 279 ( 4 sgn 28 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f44,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('/export/starexec/sandbox2/benchmark/theBenchmark.p',happens_all_defn) ).
fof(f44_nnf,plain,
! [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) ) )
| 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) )
| ~ happens(Event,Time) ) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [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) ) )
| 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) )
| ~ happens(Event,Time) ) ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c435,plain,
( X1 != n0
| X0 != pull(agent10,trolley10)
| ~ def112(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1665,plain,
( X0 != n0
| ~ def112(pull(agent10,trolley10),X0) ),
inference(equality_resolution,[status(thm)],[c435]) ).
cnf(p3666,plain,
~ def112(pull(agent10,trolley10),n0),
inference(equality_resolution,[status(thm)],[p1665]) ).
cnf(c447,plain,
( def115(X0,X1)
| happens(X0,X1)
| ~ def116(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(c451,plain,
( def116(X0,X1)
| ~ def117(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(c453,plain,
def117(X0,X1),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p793,plain,
def116(X0,X1),
inference(resolution,[status(thm)],[c451,c453]) ).
cnf(p1692,plain,
( def115(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[c447,p793]) ).
cnf(c444,plain,
( def113(X0,X1)
| ~ def115(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1724,plain,
( def113(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1692,c444]) ).
cnf(c439,plain,
( def112(X0,X1)
| ~ def113(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1742,plain,
( def112(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1724,c439]) ).
cnf(p3674,plain,
happens(pull(agent10,trolley10),n0),
inference(resolution,[status(thm)],[p3666,p1742]) ).
fof(f8,axiom,
! [Event,Time,Fluent] :
( ( initiates(Event,Fluent,Time)
& happens(Event,Time) )
=> holdsAt(Fluent,plus(Time,n1)) ),
file('/export/starexec/sandbox2/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(p3677,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent10,trolley10),X0,n0) ),
inference(resolution,[status(thm)],[p3674,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/sandbox2/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(p628,plain,
( ~ happens(push(X0,X1),X3)
| X2 != spinning(X1)
| initiates(pull(X0,X1),X2,X3) ),
inference(equality_resolution,[status(thm)],[c54]) ).
cnf(p1926,plain,
( ~ happens(push(X0,X1),X2)
| initiates(pull(X0,X1),spinning(X1),X2) ),
inference(equality_resolution,[status(thm)],[p628]) ).
cnf(c441,plain,
( X1 != n0
| X0 != push(agent10,trolley10)
| ~ def114(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1675,plain,
( X0 != n0
| ~ def114(push(agent10,trolley10),X0) ),
inference(equality_resolution,[status(thm)],[c441]) ).
cnf(p3691,plain,
~ def114(push(agent10,trolley10),n0),
inference(equality_resolution,[status(thm)],[p1675]) ).
cnf(c445,plain,
( def114(X0,X1)
| ~ def115(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1725,plain,
( def114(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1692,c445]) ).
cnf(p3699,plain,
happens(push(agent10,trolley10),n0),
inference(resolution,[status(thm)],[p3691,p1725]) ).
cnf(p15509,plain,
initiates(pull(agent10,trolley10),spinning(trolley10),n0),
inference(resolution,[status(thm)],[p1926,p3699]) ).
cnf(p28057,plain,
holdsAt(spinning(trolley10),n1),
inference(resolution,[status(thm)],[p3677,p15509]) ).
cnf(c423,plain,
( X1 != n0
| X0 != pull(agent9,trolley9)
| ~ def108(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1651,plain,
( X0 != n0
| ~ def108(pull(agent9,trolley9),X0) ),
inference(equality_resolution,[status(thm)],[c423]) ).
cnf(p3592,plain,
~ def108(pull(agent9,trolley9),n0),
inference(equality_resolution,[status(thm)],[p1651]) ).
cnf(c438,plain,
( def111(X0,X1)
| ~ def113(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1741,plain,
( def111(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1724,c438]) ).
cnf(c432,plain,
( def109(X0,X1)
| ~ def111(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1744,plain,
( def109(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1741,c432]) ).
cnf(c427,plain,
( def108(X0,X1)
| ~ def109(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1748,plain,
( def108(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1744,c427]) ).
cnf(p3596,plain,
happens(pull(agent9,trolley9),n0),
inference(resolution,[status(thm)],[p3592,p1748]) ).
cnf(p3618,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent9,trolley9),X0,n0) ),
inference(resolution,[status(thm)],[p3596,c20]) ).
cnf(c429,plain,
( X1 != n0
| X0 != push(agent9,trolley9)
| ~ def110(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1657,plain,
( X0 != n0
| ~ def110(push(agent9,trolley9),X0) ),
inference(equality_resolution,[status(thm)],[c429]) ).
cnf(p3636,plain,
~ def110(push(agent9,trolley9),n0),
inference(equality_resolution,[status(thm)],[p1657]) ).
cnf(c433,plain,
( def110(X0,X1)
| ~ def111(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1745,plain,
( def110(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1741,c433]) ).
cnf(p3640,plain,
happens(push(agent9,trolley9),n0),
inference(resolution,[status(thm)],[p3636,p1745]) ).
cnf(p15508,plain,
initiates(pull(agent9,trolley9),spinning(trolley9),n0),
inference(resolution,[status(thm)],[p1926,p3640]) ).
cnf(p27676,plain,
holdsAt(spinning(trolley9),n1),
inference(resolution,[status(thm)],[p3618,p15508]) ).
cnf(c411,plain,
( X1 != n0
| X0 != pull(agent8,trolley8)
| ~ def104(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1632,plain,
( X0 != n0
| ~ def104(pull(agent8,trolley8),X0) ),
inference(equality_resolution,[status(thm)],[c411]) ).
cnf(p3493,plain,
~ def104(pull(agent8,trolley8),n0),
inference(equality_resolution,[status(thm)],[p1632]) ).
cnf(c426,plain,
( def107(X0,X1)
| ~ def109(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1747,plain,
( def107(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1744,c426]) ).
cnf(c420,plain,
( def105(X0,X1)
| ~ def107(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1750,plain,
( def105(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1747,c420]) ).
cnf(c415,plain,
( def104(X0,X1)
| ~ def105(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1754,plain,
( def104(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1750,c415]) ).
cnf(p3497,plain,
happens(pull(agent8,trolley8),n0),
inference(resolution,[status(thm)],[p3493,p1754]) ).
cnf(p3500,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent8,trolley8),X0,n0) ),
inference(resolution,[status(thm)],[p3497,c20]) ).
cnf(c417,plain,
( X1 != n0
| X0 != push(agent8,trolley8)
| ~ def106(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1642,plain,
( X0 != n0
| ~ def106(push(agent8,trolley8),X0) ),
inference(equality_resolution,[status(thm)],[c417]) ).
cnf(p3531,plain,
~ def106(push(agent8,trolley8),n0),
inference(equality_resolution,[status(thm)],[p1642]) ).
cnf(c421,plain,
( def106(X0,X1)
| ~ def107(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1751,plain,
( def106(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1747,c421]) ).
cnf(p3535,plain,
happens(push(agent8,trolley8),n0),
inference(resolution,[status(thm)],[p3531,p1751]) ).
cnf(p15507,plain,
initiates(pull(agent8,trolley8),spinning(trolley8),n0),
inference(resolution,[status(thm)],[p1926,p3535]) ).
cnf(p26785,plain,
holdsAt(spinning(trolley8),n1),
inference(resolution,[status(thm)],[p3500,p15507]) ).
cnf(c399,plain,
( X1 != n0
| X0 != pull(agent7,trolley7)
| ~ def100(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1610,plain,
( X0 != n0
| ~ def100(pull(agent7,trolley7),X0) ),
inference(equality_resolution,[status(thm)],[c399]) ).
cnf(p3398,plain,
~ def100(pull(agent7,trolley7),n0),
inference(equality_resolution,[status(thm)],[p1610]) ).
cnf(c414,plain,
( def103(X0,X1)
| ~ def105(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1753,plain,
( def103(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1750,c414]) ).
cnf(c408,plain,
( def101(X0,X1)
| ~ def103(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1756,plain,
( def101(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1753,c408]) ).
cnf(c403,plain,
( def100(X0,X1)
| ~ def101(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1760,plain,
( def100(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1756,c403]) ).
cnf(p3402,plain,
happens(pull(agent7,trolley7),n0),
inference(resolution,[status(thm)],[p3398,p1760]) ).
cnf(p3405,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent7,trolley7),X0,n0) ),
inference(resolution,[status(thm)],[p3402,c20]) ).
cnf(c405,plain,
( X1 != n0
| X0 != push(agent7,trolley7)
| ~ def102(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1620,plain,
( X0 != n0
| ~ def102(push(agent7,trolley7),X0) ),
inference(equality_resolution,[status(thm)],[c405]) ).
cnf(p3445,plain,
~ def102(push(agent7,trolley7),n0),
inference(equality_resolution,[status(thm)],[p1620]) ).
cnf(c409,plain,
( def102(X0,X1)
| ~ def103(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1757,plain,
( def102(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1753,c409]) ).
cnf(p3449,plain,
happens(push(agent7,trolley7),n0),
inference(resolution,[status(thm)],[p3445,p1757]) ).
cnf(p15506,plain,
initiates(pull(agent7,trolley7),spinning(trolley7),n0),
inference(resolution,[status(thm)],[p1926,p3449]) ).
cnf(p26086,plain,
holdsAt(spinning(trolley7),n1),
inference(resolution,[status(thm)],[p3405,p15506]) ).
cnf(c387,plain,
( X1 != n0
| X0 != pull(agent6,trolley6)
| ~ def96(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1593,plain,
( X0 != n0
| ~ def96(pull(agent6,trolley6),X0) ),
inference(equality_resolution,[status(thm)],[c387]) ).
cnf(p3275,plain,
~ def96(pull(agent6,trolley6),n0),
inference(equality_resolution,[status(thm)],[p1593]) ).
cnf(c402,plain,
( def99(X0,X1)
| ~ def101(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1759,plain,
( def99(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1756,c402]) ).
cnf(c396,plain,
( def97(X0,X1)
| ~ def99(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1762,plain,
( def97(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1759,c396]) ).
cnf(c391,plain,
( def96(X0,X1)
| ~ def97(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1766,plain,
( def96(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1762,c391]) ).
cnf(p3299,plain,
happens(pull(agent6,trolley6),n0),
inference(resolution,[status(thm)],[p3275,p1766]) ).
cnf(p3302,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent6,trolley6),X0,n0) ),
inference(resolution,[status(thm)],[p3299,c20]) ).
cnf(c393,plain,
( X1 != n0
| X0 != push(agent6,trolley6)
| ~ def98(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1599,plain,
( X0 != n0
| ~ def98(push(agent6,trolley6),X0) ),
inference(equality_resolution,[status(thm)],[c393]) ).
cnf(p3335,plain,
~ def98(push(agent6,trolley6),n0),
inference(equality_resolution,[status(thm)],[p1599]) ).
cnf(c397,plain,
( def98(X0,X1)
| ~ def99(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1763,plain,
( def98(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1759,c397]) ).
cnf(p3339,plain,
happens(push(agent6,trolley6),n0),
inference(resolution,[status(thm)],[p3335,p1763]) ).
cnf(p15505,plain,
initiates(pull(agent6,trolley6),spinning(trolley6),n0),
inference(resolution,[status(thm)],[p1926,p3339]) ).
cnf(p25711,plain,
holdsAt(spinning(trolley6),n1),
inference(resolution,[status(thm)],[p3302,p15505]) ).
cnf(c375,plain,
( X1 != n0
| X0 != pull(agent5,trolley5)
| ~ def92(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1579,plain,
( X0 != n0
| ~ def92(pull(agent5,trolley5),X0) ),
inference(equality_resolution,[status(thm)],[c375]) ).
cnf(p3180,plain,
~ def92(pull(agent5,trolley5),n0),
inference(equality_resolution,[status(thm)],[p1579]) ).
cnf(c390,plain,
( def95(X0,X1)
| ~ def97(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1765,plain,
( def95(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1762,c390]) ).
cnf(c384,plain,
( def93(X0,X1)
| ~ def95(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1770,plain,
( def93(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1765,c384]) ).
cnf(c379,plain,
( def92(X0,X1)
| ~ def93(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1774,plain,
( def92(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1770,c379]) ).
cnf(p3184,plain,
happens(pull(agent5,trolley5),n0),
inference(resolution,[status(thm)],[p3180,p1774]) ).
cnf(p3195,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent5,trolley5),X0,n0) ),
inference(resolution,[status(thm)],[p3184,c20]) ).
cnf(c381,plain,
( X1 != n0
| X0 != push(agent5,trolley5)
| ~ def94(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1585,plain,
( X0 != n0
| ~ def94(push(agent5,trolley5),X0) ),
inference(equality_resolution,[status(thm)],[c381]) ).
cnf(p3221,plain,
~ def94(push(agent5,trolley5),n0),
inference(equality_resolution,[status(thm)],[p1585]) ).
cnf(c385,plain,
( def94(X0,X1)
| ~ def95(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1771,plain,
( def94(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1765,c385]) ).
cnf(p3225,plain,
happens(push(agent5,trolley5),n0),
inference(resolution,[status(thm)],[p3221,p1771]) ).
cnf(p15504,plain,
initiates(pull(agent5,trolley5),spinning(trolley5),n0),
inference(resolution,[status(thm)],[p1926,p3225]) ).
cnf(p24968,plain,
holdsAt(spinning(trolley5),n1),
inference(resolution,[status(thm)],[p3195,p15504]) ).
cnf(c363,plain,
( X1 != n0
| X0 != pull(agent4,trolley4)
| ~ def88(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1566,plain,
( X0 != n0
| ~ def88(pull(agent4,trolley4),X0) ),
inference(equality_resolution,[status(thm)],[c363]) ).
cnf(p3061,plain,
~ def88(pull(agent4,trolley4),n0),
inference(equality_resolution,[status(thm)],[p1566]) ).
cnf(c378,plain,
( def91(X0,X1)
| ~ def93(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1773,plain,
( def91(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1770,c378]) ).
cnf(c372,plain,
( def89(X0,X1)
| ~ def91(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1777,plain,
( def89(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1773,c372]) ).
cnf(c367,plain,
( def88(X0,X1)
| ~ def89(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1781,plain,
( def88(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1777,c367]) ).
cnf(p3065,plain,
happens(pull(agent4,trolley4),n0),
inference(resolution,[status(thm)],[p3061,p1781]) ).
cnf(p3068,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent4,trolley4),X0,n0) ),
inference(resolution,[status(thm)],[p3065,c20]) ).
cnf(c369,plain,
( X1 != n0
| X0 != push(agent4,trolley4)
| ~ def90(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1571,plain,
( X0 != n0
| ~ def90(push(agent4,trolley4),X0) ),
inference(equality_resolution,[status(thm)],[c369]) ).
cnf(p3123,plain,
~ def90(push(agent4,trolley4),n0),
inference(equality_resolution,[status(thm)],[p1571]) ).
cnf(c373,plain,
( def90(X0,X1)
| ~ def91(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1778,plain,
( def90(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1773,c373]) ).
cnf(p3127,plain,
happens(push(agent4,trolley4),n0),
inference(resolution,[status(thm)],[p3123,p1778]) ).
cnf(p15503,plain,
initiates(pull(agent4,trolley4),spinning(trolley4),n0),
inference(resolution,[status(thm)],[p1926,p3127]) ).
cnf(p24369,plain,
holdsAt(spinning(trolley4),n1),
inference(resolution,[status(thm)],[p3068,p15503]) ).
cnf(c351,plain,
( X1 != n0
| X0 != pull(agent3,trolley3)
| ~ def84(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1545,plain,
( X0 != n0
| ~ def84(pull(agent3,trolley3),X0) ),
inference(equality_resolution,[status(thm)],[c351]) ).
cnf(p2958,plain,
~ def84(pull(agent3,trolley3),n0),
inference(equality_resolution,[status(thm)],[p1545]) ).
cnf(c366,plain,
( def87(X0,X1)
| ~ def89(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1780,plain,
( def87(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1777,c366]) ).
cnf(c360,plain,
( def85(X0,X1)
| ~ def87(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1783,plain,
( def85(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1780,c360]) ).
cnf(c355,plain,
( def84(X0,X1)
| ~ def85(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1787,plain,
( def84(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1783,c355]) ).
cnf(p2962,plain,
happens(pull(agent3,trolley3),n0),
inference(resolution,[status(thm)],[p2958,p1787]) ).
cnf(p2965,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent3,trolley3),X0,n0) ),
inference(resolution,[status(thm)],[p2962,c20]) ).
cnf(c357,plain,
( X1 != n0
| X0 != push(agent3,trolley3)
| ~ def86(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1555,plain,
( X0 != n0
| ~ def86(push(agent3,trolley3),X0) ),
inference(equality_resolution,[status(thm)],[c357]) ).
cnf(p3001,plain,
~ def86(push(agent3,trolley3),n0),
inference(equality_resolution,[status(thm)],[p1555]) ).
cnf(c361,plain,
( def86(X0,X1)
| ~ def87(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1784,plain,
( def86(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1780,c361]) ).
cnf(p3005,plain,
happens(push(agent3,trolley3),n0),
inference(resolution,[status(thm)],[p3001,p1784]) ).
cnf(p15502,plain,
initiates(pull(agent3,trolley3),spinning(trolley3),n0),
inference(resolution,[status(thm)],[p1926,p3005]) ).
cnf(p23966,plain,
holdsAt(spinning(trolley3),n1),
inference(resolution,[status(thm)],[p2965,p15502]) ).
cnf(c339,plain,
( X1 != n0
| X0 != pull(agent2,trolley2)
| ~ def80(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1523,plain,
( X0 != n0
| ~ def80(pull(agent2,trolley2),X0) ),
inference(equality_resolution,[status(thm)],[c339]) ).
cnf(p2831,plain,
~ def80(pull(agent2,trolley2),n0),
inference(equality_resolution,[status(thm)],[p1523]) ).
cnf(c354,plain,
( def83(X0,X1)
| ~ def85(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1786,plain,
( def83(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1783,c354]) ).
cnf(c348,plain,
( def81(X0,X1)
| ~ def83(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1790,plain,
( def81(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1786,c348]) ).
cnf(c343,plain,
( def80(X0,X1)
| ~ def81(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1794,plain,
( def80(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1790,c343]) ).
cnf(p2835,plain,
happens(pull(agent2,trolley2),n0),
inference(resolution,[status(thm)],[p2831,p1794]) ).
cnf(p2838,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent2,trolley2),X0,n0) ),
inference(resolution,[status(thm)],[p2835,c20]) ).
cnf(c345,plain,
( X1 != n0
| X0 != push(agent2,trolley2)
| ~ def82(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1533,plain,
( X0 != n0
| ~ def82(push(agent2,trolley2),X0) ),
inference(equality_resolution,[status(thm)],[c345]) ).
cnf(p2892,plain,
~ def82(push(agent2,trolley2),n0),
inference(equality_resolution,[status(thm)],[p1533]) ).
cnf(c349,plain,
( def82(X0,X1)
| ~ def83(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1791,plain,
( def82(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1786,c349]) ).
cnf(p2899,plain,
happens(push(agent2,trolley2),n0),
inference(resolution,[status(thm)],[p2892,p1791]) ).
cnf(p15501,plain,
initiates(pull(agent2,trolley2),spinning(trolley2),n0),
inference(resolution,[status(thm)],[p1926,p2899]) ).
cnf(p23414,plain,
holdsAt(spinning(trolley2),n1),
inference(resolution,[status(thm)],[p2838,p15501]) ).
cnf(c330,plain,
( X1 != n0
| X0 != pull(agent1,trolley1)
| ~ def77(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1471,plain,
( X0 != n0
| ~ def77(pull(agent1,trolley1),X0) ),
inference(equality_resolution,[status(thm)],[c330]) ).
cnf(p2720,plain,
~ def77(pull(agent1,trolley1),n0),
inference(equality_resolution,[status(thm)],[p1471]) ).
cnf(c342,plain,
( def79(X0,X1)
| ~ def81(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1793,plain,
( def79(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1790,c342]) ).
cnf(c336,plain,
( def77(X0,X1)
| ~ def79(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1796,plain,
( def77(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1793,c336]) ).
cnf(p2724,plain,
happens(pull(agent1,trolley1),n0),
inference(resolution,[status(thm)],[p2720,p1796]) ).
cnf(p2727,plain,
( holdsAt(X0,n1)
| ~ initiates(pull(agent1,trolley1),X0,n0) ),
inference(resolution,[status(thm)],[p2724,c20]) ).
cnf(c333,plain,
( X1 != n0
| X0 != push(agent1,trolley1)
| ~ def78(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1493,plain,
( X0 != n0
| ~ def78(push(agent1,trolley1),X0) ),
inference(equality_resolution,[status(thm)],[c333]) ).
cnf(p2765,plain,
~ def78(push(agent1,trolley1),n0),
inference(equality_resolution,[status(thm)],[p1493]) ).
cnf(c337,plain,
( def78(X0,X1)
| ~ def79(X0,X1) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,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])],[f44_sk]) ).
cnf(p1797,plain,
( def78(X0,X1)
| happens(X0,X1) ),
inference(resolution,[status(thm)],[p1793,c337]) ).
cnf(p2769,plain,
happens(push(agent1,trolley1),n0),
inference(resolution,[status(thm)],[p2765,p1797]) ).
cnf(p15500,plain,
initiates(pull(agent1,trolley1),spinning(trolley1),n0),
inference(resolution,[status(thm)],[p1926,p2769]) ).
cnf(p22550,plain,
holdsAt(spinning(trolley1),n1),
inference(resolution,[status(thm)],[p2727,p15500]) ).
fof(f48,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('/export/starexec/sandbox2/benchmark/theBenchmark.p',spinning_3) ).
fof(f48_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(negated_conjecture,[status(cth)],[f48]) ).
fof(f48_nnf,plain,
( ~ 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(nnf_transformation,[status(thm)],[f48_neg]) ).
fof(f48_sk,plain,
( ~ 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(skolemisation,[status(esa)],[f48_nnf]) ).
cnf(c575,plain,
( ~ 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(cnf_transformation,[status(esa)],[f48_sk]) ).
cnf(p22560,plain,
( ~ 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) ),
inference(resolution,[status(thm)],[p22550,c575]) ).
cnf(p23427,plain,
( ~ 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) ),
inference(resolution,[status(thm)],[p23414,p22560]) ).
cnf(p23978,plain,
( ~ 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) ),
inference(resolution,[status(thm)],[p23966,p23427]) ).
cnf(p24380,plain,
( ~ holdsAt(spinning(trolley10),n1)
| ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1)
| ~ holdsAt(spinning(trolley5),n1) ),
inference(resolution,[status(thm)],[p24369,p23978]) ).
cnf(p24978,plain,
( ~ holdsAt(spinning(trolley10),n1)
| ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1)
| ~ holdsAt(spinning(trolley6),n1) ),
inference(resolution,[status(thm)],[p24968,p24380]) ).
cnf(p25720,plain,
( ~ holdsAt(spinning(trolley10),n1)
| ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1)
| ~ holdsAt(spinning(trolley7),n1) ),
inference(resolution,[status(thm)],[p25711,p24978]) ).
cnf(p26094,plain,
( ~ holdsAt(spinning(trolley10),n1)
| ~ holdsAt(spinning(trolley9),n1)
| ~ holdsAt(spinning(trolley8),n1) ),
inference(resolution,[status(thm)],[p26086,p25720]) ).
cnf(p26792,plain,
( ~ holdsAt(spinning(trolley10),n1)
| ~ holdsAt(spinning(trolley9),n1) ),
inference(resolution,[status(thm)],[p26785,p26094]) ).
cnf(p27682,plain,
~ holdsAt(spinning(trolley10),n1),
inference(resolution,[status(thm)],[p27676,p26792]) ).
cnf(p28062,plain,
$false,
inference(resolution,[status(thm)],[p28057,p27682]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR024+1.010 : TPTP v9.3.1. Bugfixed v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.34 % Computer : n001.cluster.edu
% 0.10/0.34 % Model : x86_64 x86_64
% 0.10/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.34 % Memory : 8046.5625MB
% 0.10/0.34 % OS : Linux 6.8.0-71-generic
% 0.10/0.34 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Fri Sep 25 08:13:24 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 117.50/16.46 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 117.50/16.46 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------