%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : CSR024+1.009 : TPTP v9.3.1. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n019.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:09:54 PM UTC 2026
% Result : Theorem 6.90s 2.14s
% Output : CNFRefutation 11.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 23
% Syntax : Number of formulae : 297 ( 82 unt; 18 def)
% Number of atoms : 953 ( 378 equ)
% Maximal formula atoms : 44 ( 3 avg)
% Number of connectives : 1068 ( 412 ~; 441 |; 192 &)
% ( 22 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 23 ( 21 usr; 1 prp; 0-5 aty)
% Number of functors : 28 ( 28 usr; 20 con; 0-3 aty)
% Number of variables : 418 ( 0 sgn 410 !; 8 ?; 147 :)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [X0,X1,X2] :
( ( initiates(X0,X2,X1)
& happens(X0,X1) )
=> holdsAt(X2,plus(X1,n1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR001+0.ax',happens_holds) ).
fof(f23,axiom,
plus(n0,n1) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',plus0_1) ).
fof(f45,axiom,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ? [X3,X4] :
( ( happens(push(X3,X4),X2)
& X1 = spinning(X4)
& X0 = pull(X3,X4) )
| ( ~ happens(push(X3,X4),X2)
& X1 = backwards(X4)
& X0 = pull(X3,X4) )
| ( ~ happens(pull(X3,X4),X2)
& X1 = forwards(X4)
& X0 = push(X3,X4) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',initiates_all_defn) ).
fof(f48,axiom,
! [X0,X1] :
( happens(X0,X1)
<=> ( ( X1 = n0
& X0 = push(agent9,trolley9) )
| ( X1 = n0
& X0 = pull(agent9,trolley9) )
| ( X1 = n0
& X0 = push(agent8,trolley8) )
| ( X1 = n0
& X0 = pull(agent8,trolley8) )
| ( X1 = n0
& X0 = push(agent7,trolley7) )
| ( X1 = n0
& X0 = pull(agent7,trolley7) )
| ( X1 = n0
& X0 = push(agent6,trolley6) )
| ( X1 = n0
& X0 = pull(agent6,trolley6) )
| ( X1 = n0
& X0 = push(agent5,trolley5) )
| ( X1 = n0
& X0 = pull(agent5,trolley5) )
| ( X1 = n0
& X0 = push(agent4,trolley4) )
| ( X1 = n0
& X0 = pull(agent4,trolley4) )
| ( X1 = n0
& X0 = push(agent3,trolley3) )
| ( X1 = n0
& X0 = pull(agent3,trolley3) )
| ( X1 = n0
& X0 = push(agent2,trolley2) )
| ( X1 = n0
& X0 = pull(agent2,trolley2) )
| ( X1 = n0
& X0 = push(agent1,trolley1) )
| ( X1 = n0
& X0 = pull(agent1,trolley1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',happens_all_defn) ).
fof(f58,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(f59,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)],[f58]) ).
fof(f60,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(ennf_transformation,[],[f59]) ).
fof(f64,plain,
! [X0,X1,X2] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(ennf_transformation,[],[f9]) ).
fof(f65,plain,
! [X0,X1,X2] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(flattening,[],[f64]) ).
fof(f145,plain,
! [X0,X1,X2] :
( ( ~ initiates(X0,X1,X2)
| ? [X3,X4] :
( sP6(X0,X4,X3,X1,X2)
| sP7(X0,X4,X3,X1,X2)
| ( ~ happens(pull(X3,X4),X2)
& X1 = forwards(X4)
& X0 = push(X3,X4) ) ) )
& ( ! [X3,X4] :
( ~ sP6(X0,X4,X3,X1,X2)
& ~ sP7(X0,X4,X3,X1,X2)
& ( happens(pull(X3,X4),X2)
| forwards(X4) != X1
| push(X3,X4) != X0 ) )
| initiates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f91]) ).
fof(f146,plain,
! [X0,X1,X2] :
( ( ~ initiates(X0,X1,X2)
| ? [X5,X6] :
( sP6(X0,X6,X5,X1,X2)
| sP7(X0,X6,X5,X1,X2)
| ( ~ happens(pull(X5,X6),X2)
& forwards(X6) = X1
& push(X5,X6) = X0 ) ) )
& ( ! [X3,X4] :
( ~ sP6(X0,X4,X3,X1,X2)
& ~ sP7(X0,X4,X3,X1,X2)
& ( happens(pull(X3,X4),X2)
| forwards(X4) != X1
| push(X3,X4) != X0 ) )
| initiates(X0,X1,X2) ) ),
inference(rectify,[],[f145]) ).
fof(f147,plain,
! [X0,X1,X2] :
( ( ~ initiates(X0,X1,X2)
| sP6(X0,sK35(X0,X1,X2),sK34(X0,X1,X2),X1,X2)
| sP7(X0,sK35(X0,X1,X2),sK34(X0,X1,X2),X1,X2)
| ( ~ happens(pull(sK34(X0,X1,X2),sK35(X0,X1,X2)),X2)
& forwards(sK35(X0,X1,X2)) = X1
& push(sK34(X0,X1,X2),sK35(X0,X1,X2)) = X0 ) )
& ( ! [X3,X4] :
( ~ sP6(X0,X4,X3,X1,X2)
& ~ sP7(X0,X4,X3,X1,X2)
& ( happens(pull(X3,X4),X2)
| forwards(X4) != X1
| push(X3,X4) != X0 ) )
| initiates(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34,sK35]),skolemize(X5,sK34(X0,X1,X2)),skolemize(X6,sK35(X0,X1,X2))],[f146]) ).
fof(f179,plain,
! [X0,X1] :
( ( ~ sP31(X0,X1)
| sP16(X0,X1)
| sP17(X0,X1)
| sP18(X0,X1)
| sP19(X0,X1)
| sP20(X0,X1)
| sP21(X0,X1)
| sP22(X0,X1)
| sP23(X0,X1)
| sP24(X0,X1)
| sP25(X0,X1)
| sP26(X0,X1)
| sP27(X0,X1)
| sP28(X0,X1)
| sP29(X0,X1)
| sP30(X0,X1)
| ( X1 = n0
& X0 = pull(agent2,trolley2) )
| ( X1 = n0
& X0 = push(agent1,trolley1) )
| ( X1 = n0
& X0 = pull(agent1,trolley1) ) )
& ( ( ~ sP16(X0,X1)
& ~ sP17(X0,X1)
& ~ sP18(X0,X1)
& ~ sP19(X0,X1)
& ~ sP20(X0,X1)
& ~ sP21(X0,X1)
& ~ sP22(X0,X1)
& ~ sP23(X0,X1)
& ~ sP24(X0,X1)
& ~ sP25(X0,X1)
& ~ sP26(X0,X1)
& ~ sP27(X0,X1)
& ~ sP28(X0,X1)
& ~ sP29(X0,X1)
& ~ sP30(X0,X1)
& ( n0 != X1
| pull(agent2,trolley2) != X0 )
& ( n0 != X1
| push(agent1,trolley1) != X0 )
& ( n0 != X1
| pull(agent1,trolley1) != X0 ) )
| sP31(X0,X1) ) ),
inference(nnf_transformation,[],[f117]) ).
fof(f180,plain,
! [X0,X1] :
( ( ~ sP31(X0,X1)
| sP16(X0,X1)
| sP17(X0,X1)
| sP18(X0,X1)
| sP19(X0,X1)
| sP20(X0,X1)
| sP21(X0,X1)
| sP22(X0,X1)
| sP23(X0,X1)
| sP24(X0,X1)
| sP25(X0,X1)
| sP26(X0,X1)
| sP27(X0,X1)
| sP28(X0,X1)
| sP29(X0,X1)
| sP30(X0,X1)
| ( X1 = n0
& X0 = pull(agent2,trolley2) )
| ( X1 = n0
& X0 = push(agent1,trolley1) )
| ( X1 = n0
& X0 = pull(agent1,trolley1) ) )
& ( ( ~ sP16(X0,X1)
& ~ sP17(X0,X1)
& ~ sP18(X0,X1)
& ~ sP19(X0,X1)
& ~ sP20(X0,X1)
& ~ sP21(X0,X1)
& ~ sP22(X0,X1)
& ~ sP23(X0,X1)
& ~ sP24(X0,X1)
& ~ sP25(X0,X1)
& ~ sP26(X0,X1)
& ~ sP27(X0,X1)
& ~ sP28(X0,X1)
& ~ sP29(X0,X1)
& ~ sP30(X0,X1)
& ( n0 != X1
| pull(agent2,trolley2) != X0 )
& ( n0 != X1
| push(agent1,trolley1) != X0 )
& ( n0 != X1
| pull(agent1,trolley1) != X0 ) )
| sP31(X0,X1) ) ),
inference(flattening,[],[f179]) ).
fof(f181,plain,
! [X0,X1] :
( ( ~ sP30(X0,X1)
| ( X1 = n0
& X0 = push(agent2,trolley2) ) )
& ( n0 != X1
| push(agent2,trolley2) != X0
| sP30(X0,X1) ) ),
inference(nnf_transformation,[],[f116]) ).
fof(f182,plain,
! [X0,X1] :
( ( ~ sP30(X0,X1)
| ( X1 = n0
& X0 = push(agent2,trolley2) ) )
& ( n0 != X1
| push(agent2,trolley2) != X0
| sP30(X0,X1) ) ),
inference(flattening,[],[f181]) ).
fof(f183,plain,
! [X0,X1] :
( ( ~ sP29(X0,X1)
| ( X1 = n0
& X0 = pull(agent3,trolley3) ) )
& ( n0 != X1
| pull(agent3,trolley3) != X0
| sP29(X0,X1) ) ),
inference(nnf_transformation,[],[f115]) ).
fof(f184,plain,
! [X0,X1] :
( ( ~ sP29(X0,X1)
| ( X1 = n0
& X0 = pull(agent3,trolley3) ) )
& ( n0 != X1
| pull(agent3,trolley3) != X0
| sP29(X0,X1) ) ),
inference(flattening,[],[f183]) ).
fof(f185,plain,
! [X0,X1] :
( ( ~ sP28(X0,X1)
| ( X1 = n0
& X0 = push(agent3,trolley3) ) )
& ( n0 != X1
| push(agent3,trolley3) != X0
| sP28(X0,X1) ) ),
inference(nnf_transformation,[],[f114]) ).
fof(f186,plain,
! [X0,X1] :
( ( ~ sP28(X0,X1)
| ( X1 = n0
& X0 = push(agent3,trolley3) ) )
& ( n0 != X1
| push(agent3,trolley3) != X0
| sP28(X0,X1) ) ),
inference(flattening,[],[f185]) ).
fof(f187,plain,
! [X0,X1] :
( ( ~ sP27(X0,X1)
| ( X1 = n0
& X0 = pull(agent4,trolley4) ) )
& ( n0 != X1
| pull(agent4,trolley4) != X0
| sP27(X0,X1) ) ),
inference(nnf_transformation,[],[f113]) ).
fof(f188,plain,
! [X0,X1] :
( ( ~ sP27(X0,X1)
| ( X1 = n0
& X0 = pull(agent4,trolley4) ) )
& ( n0 != X1
| pull(agent4,trolley4) != X0
| sP27(X0,X1) ) ),
inference(flattening,[],[f187]) ).
fof(f189,plain,
! [X0,X1] :
( ( ~ sP26(X0,X1)
| ( X1 = n0
& X0 = push(agent4,trolley4) ) )
& ( n0 != X1
| push(agent4,trolley4) != X0
| sP26(X0,X1) ) ),
inference(nnf_transformation,[],[f112]) ).
fof(f190,plain,
! [X0,X1] :
( ( ~ sP26(X0,X1)
| ( X1 = n0
& X0 = push(agent4,trolley4) ) )
& ( n0 != X1
| push(agent4,trolley4) != X0
| sP26(X0,X1) ) ),
inference(flattening,[],[f189]) ).
fof(f191,plain,
! [X0,X1] :
( ( ~ sP25(X0,X1)
| ( X1 = n0
& X0 = pull(agent5,trolley5) ) )
& ( n0 != X1
| pull(agent5,trolley5) != X0
| sP25(X0,X1) ) ),
inference(nnf_transformation,[],[f111]) ).
fof(f192,plain,
! [X0,X1] :
( ( ~ sP25(X0,X1)
| ( X1 = n0
& X0 = pull(agent5,trolley5) ) )
& ( n0 != X1
| pull(agent5,trolley5) != X0
| sP25(X0,X1) ) ),
inference(flattening,[],[f191]) ).
fof(f193,plain,
! [X0,X1] :
( ( ~ sP24(X0,X1)
| ( X1 = n0
& X0 = push(agent5,trolley5) ) )
& ( n0 != X1
| push(agent5,trolley5) != X0
| sP24(X0,X1) ) ),
inference(nnf_transformation,[],[f110]) ).
fof(f194,plain,
! [X0,X1] :
( ( ~ sP24(X0,X1)
| ( X1 = n0
& X0 = push(agent5,trolley5) ) )
& ( n0 != X1
| push(agent5,trolley5) != X0
| sP24(X0,X1) ) ),
inference(flattening,[],[f193]) ).
fof(f195,plain,
! [X0,X1] :
( ( ~ sP23(X0,X1)
| ( X1 = n0
& X0 = pull(agent6,trolley6) ) )
& ( n0 != X1
| pull(agent6,trolley6) != X0
| sP23(X0,X1) ) ),
inference(nnf_transformation,[],[f109]) ).
fof(f196,plain,
! [X0,X1] :
( ( ~ sP23(X0,X1)
| ( X1 = n0
& X0 = pull(agent6,trolley6) ) )
& ( n0 != X1
| pull(agent6,trolley6) != X0
| sP23(X0,X1) ) ),
inference(flattening,[],[f195]) ).
fof(f197,plain,
! [X0,X1] :
( ( ~ sP22(X0,X1)
| ( X1 = n0
& X0 = push(agent6,trolley6) ) )
& ( n0 != X1
| push(agent6,trolley6) != X0
| sP22(X0,X1) ) ),
inference(nnf_transformation,[],[f108]) ).
fof(f198,plain,
! [X0,X1] :
( ( ~ sP22(X0,X1)
| ( X1 = n0
& X0 = push(agent6,trolley6) ) )
& ( n0 != X1
| push(agent6,trolley6) != X0
| sP22(X0,X1) ) ),
inference(flattening,[],[f197]) ).
fof(f199,plain,
! [X0,X1] :
( ( ~ sP21(X0,X1)
| ( X1 = n0
& X0 = pull(agent7,trolley7) ) )
& ( n0 != X1
| pull(agent7,trolley7) != X0
| sP21(X0,X1) ) ),
inference(nnf_transformation,[],[f107]) ).
fof(f200,plain,
! [X0,X1] :
( ( ~ sP21(X0,X1)
| ( X1 = n0
& X0 = pull(agent7,trolley7) ) )
& ( n0 != X1
| pull(agent7,trolley7) != X0
| sP21(X0,X1) ) ),
inference(flattening,[],[f199]) ).
fof(f201,plain,
! [X0,X1] :
( ( ~ sP20(X0,X1)
| ( X1 = n0
& X0 = push(agent7,trolley7) ) )
& ( n0 != X1
| push(agent7,trolley7) != X0
| sP20(X0,X1) ) ),
inference(nnf_transformation,[],[f106]) ).
fof(f202,plain,
! [X0,X1] :
( ( ~ sP20(X0,X1)
| ( X1 = n0
& X0 = push(agent7,trolley7) ) )
& ( n0 != X1
| push(agent7,trolley7) != X0
| sP20(X0,X1) ) ),
inference(flattening,[],[f201]) ).
fof(f203,plain,
! [X0,X1] :
( ( ~ sP19(X0,X1)
| ( X1 = n0
& X0 = pull(agent8,trolley8) ) )
& ( n0 != X1
| pull(agent8,trolley8) != X0
| sP19(X0,X1) ) ),
inference(nnf_transformation,[],[f105]) ).
fof(f204,plain,
! [X0,X1] :
( ( ~ sP19(X0,X1)
| ( X1 = n0
& X0 = pull(agent8,trolley8) ) )
& ( n0 != X1
| pull(agent8,trolley8) != X0
| sP19(X0,X1) ) ),
inference(flattening,[],[f203]) ).
fof(f205,plain,
! [X0,X1] :
( ( ~ sP18(X0,X1)
| ( X1 = n0
& X0 = push(agent8,trolley8) ) )
& ( n0 != X1
| push(agent8,trolley8) != X0
| sP18(X0,X1) ) ),
inference(nnf_transformation,[],[f104]) ).
fof(f206,plain,
! [X0,X1] :
( ( ~ sP18(X0,X1)
| ( X1 = n0
& X0 = push(agent8,trolley8) ) )
& ( n0 != X1
| push(agent8,trolley8) != X0
| sP18(X0,X1) ) ),
inference(flattening,[],[f205]) ).
fof(f207,plain,
! [X0,X1] :
( ( ~ sP17(X0,X1)
| ( X1 = n0
& X0 = pull(agent9,trolley9) ) )
& ( n0 != X1
| pull(agent9,trolley9) != X0
| sP17(X0,X1) ) ),
inference(nnf_transformation,[],[f103]) ).
fof(f208,plain,
! [X0,X1] :
( ( ~ sP17(X0,X1)
| ( X1 = n0
& X0 = pull(agent9,trolley9) ) )
& ( n0 != X1
| pull(agent9,trolley9) != X0
| sP17(X0,X1) ) ),
inference(flattening,[],[f207]) ).
fof(f211,plain,
! [X0,X1] :
( ( ~ happens(X0,X1)
| sP31(X0,X1) )
& ( ~ sP31(X0,X1)
| happens(X0,X1) ) ),
inference(nnf_transformation,[],[f118]) ).
fof(f318,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,[],[f60]) ).
fof(f324,plain,
n1 = plus(n0,n1),
inference(cnf_transformation,[],[f23]) ).
fof(f370,plain,
! [X2,X3,X0,X1,X4] :
( ~ sP6(X0,X4,X3,X1,X2)
| initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f147]) ).
fof(f423,plain,
! [X2,X0,X1] :
( ~ initiates(X0,X2,X1)
| ~ happens(X0,X1)
| holdsAt(X2,plus(X1,n1)) ),
inference(cnf_transformation,[],[f65]) ).
fof(f441,plain,
! [X0,X1] :
( ~ sP16(X0,X1)
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f442,plain,
! [X0,X1] :
( ~ sP17(X0,X1)
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f443,plain,
! [X0,X1] :
( ~ sP18(X0,X1)
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f444,plain,
! [X0,X1] :
( ~ sP19(X0,X1)
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f445,plain,
! [X0,X1] :
( ~ sP20(X0,X1)
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f446,plain,
! [X0,X1] :
( ~ sP21(X0,X1)
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f447,plain,
! [X0,X1] :
( ~ sP22(X0,X1)
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f448,plain,
! [X0,X1] :
( ~ sP23(X0,X1)
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f449,plain,
! [X0,X1] :
( ~ sP24(X0,X1)
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f450,plain,
! [X0,X1] :
( ~ sP25(X0,X1)
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f451,plain,
! [X0,X1] :
( ~ sP26(X0,X1)
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f452,plain,
! [X0,X1] :
( ~ sP27(X0,X1)
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f453,plain,
! [X0,X1] :
( ~ sP28(X0,X1)
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f454,plain,
! [X0,X1] :
( ~ sP29(X0,X1)
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f455,plain,
! [X0,X1] :
( ~ sP30(X0,X1)
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f456,plain,
! [X0,X1] :
( n0 != X1
| pull(agent2,trolley2) != X0
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f457,plain,
! [X0,X1] :
( n0 != X1
| push(agent1,trolley1) != X0
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f458,plain,
! [X0,X1] :
( n0 != X1
| pull(agent1,trolley1) != X0
| sP31(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f461,plain,
! [X0,X1] :
( n0 != X1
| push(agent2,trolley2) != X0
| sP30(X0,X1) ),
inference(cnf_transformation,[],[f182]) ).
fof(f464,plain,
! [X0,X1] :
( n0 != X1
| pull(agent3,trolley3) != X0
| sP29(X0,X1) ),
inference(cnf_transformation,[],[f184]) ).
fof(f467,plain,
! [X0,X1] :
( n0 != X1
| push(agent3,trolley3) != X0
| sP28(X0,X1) ),
inference(cnf_transformation,[],[f186]) ).
fof(f470,plain,
! [X0,X1] :
( n0 != X1
| pull(agent4,trolley4) != X0
| sP27(X0,X1) ),
inference(cnf_transformation,[],[f188]) ).
fof(f473,plain,
! [X0,X1] :
( n0 != X1
| push(agent4,trolley4) != X0
| sP26(X0,X1) ),
inference(cnf_transformation,[],[f190]) ).
fof(f476,plain,
! [X0,X1] :
( n0 != X1
| pull(agent5,trolley5) != X0
| sP25(X0,X1) ),
inference(cnf_transformation,[],[f192]) ).
fof(f479,plain,
! [X0,X1] :
( n0 != X1
| push(agent5,trolley5) != X0
| sP24(X0,X1) ),
inference(cnf_transformation,[],[f194]) ).
fof(f482,plain,
! [X0,X1] :
( n0 != X1
| pull(agent6,trolley6) != X0
| sP23(X0,X1) ),
inference(cnf_transformation,[],[f196]) ).
fof(f485,plain,
! [X0,X1] :
( n0 != X1
| push(agent6,trolley6) != X0
| sP22(X0,X1) ),
inference(cnf_transformation,[],[f198]) ).
fof(f488,plain,
! [X0,X1] :
( n0 != X1
| pull(agent7,trolley7) != X0
| sP21(X0,X1) ),
inference(cnf_transformation,[],[f200]) ).
fof(f491,plain,
! [X0,X1] :
( n0 != X1
| push(agent7,trolley7) != X0
| sP20(X0,X1) ),
inference(cnf_transformation,[],[f202]) ).
fof(f494,plain,
! [X0,X1] :
( n0 != X1
| pull(agent8,trolley8) != X0
| sP19(X0,X1) ),
inference(cnf_transformation,[],[f204]) ).
fof(f497,plain,
! [X0,X1] :
( n0 != X1
| push(agent8,trolley8) != X0
| sP18(X0,X1) ),
inference(cnf_transformation,[],[f206]) ).
fof(f500,plain,
! [X0,X1] :
( n0 != X1
| pull(agent9,trolley9) != X0
| sP17(X0,X1) ),
inference(cnf_transformation,[],[f208]) ).
fof(f505,plain,
! [X0,X1] :
( ~ sP31(X0,X1)
| happens(X0,X1) ),
inference(cnf_transformation,[],[f211]) ).
fof(f560,plain,
! [X1] :
( n0 != X1
| sP31(pull(agent1,trolley1),X1) ),
inference(equality_resolution,[],[f458]) ).
fof(f561,plain,
sP31(pull(agent1,trolley1),n0),
inference(equality_resolution,[],[f560]) ).
fof(f562,plain,
! [X1] :
( n0 != X1
| sP31(push(agent1,trolley1),X1) ),
inference(equality_resolution,[],[f457]) ).
fof(f563,plain,
sP31(push(agent1,trolley1),n0),
inference(equality_resolution,[],[f562]) ).
fof(f564,plain,
! [X1] :
( n0 != X1
| sP31(pull(agent2,trolley2),X1) ),
inference(equality_resolution,[],[f456]) ).
fof(f565,plain,
sP31(pull(agent2,trolley2),n0),
inference(equality_resolution,[],[f564]) ).
fof(f566,plain,
! [X1] :
( n0 != X1
| sP30(push(agent2,trolley2),X1) ),
inference(equality_resolution,[],[f461]) ).
fof(f567,plain,
sP30(push(agent2,trolley2),n0),
inference(equality_resolution,[],[f566]) ).
fof(f568,plain,
! [X1] :
( n0 != X1
| sP29(pull(agent3,trolley3),X1) ),
inference(equality_resolution,[],[f464]) ).
fof(f569,plain,
sP29(pull(agent3,trolley3),n0),
inference(equality_resolution,[],[f568]) ).
fof(f570,plain,
! [X1] :
( n0 != X1
| sP28(push(agent3,trolley3),X1) ),
inference(equality_resolution,[],[f467]) ).
fof(f571,plain,
sP28(push(agent3,trolley3),n0),
inference(equality_resolution,[],[f570]) ).
fof(f572,plain,
! [X1] :
( n0 != X1
| sP27(pull(agent4,trolley4),X1) ),
inference(equality_resolution,[],[f470]) ).
fof(f573,plain,
sP27(pull(agent4,trolley4),n0),
inference(equality_resolution,[],[f572]) ).
fof(f574,plain,
! [X1] :
( n0 != X1
| sP26(push(agent4,trolley4),X1) ),
inference(equality_resolution,[],[f473]) ).
fof(f575,plain,
sP26(push(agent4,trolley4),n0),
inference(equality_resolution,[],[f574]) ).
fof(f576,plain,
! [X1] :
( n0 != X1
| sP25(pull(agent5,trolley5),X1) ),
inference(equality_resolution,[],[f476]) ).
fof(f577,plain,
sP25(pull(agent5,trolley5),n0),
inference(equality_resolution,[],[f576]) ).
fof(f578,plain,
! [X1] :
( n0 != X1
| sP24(push(agent5,trolley5),X1) ),
inference(equality_resolution,[],[f479]) ).
fof(f579,plain,
sP24(push(agent5,trolley5),n0),
inference(equality_resolution,[],[f578]) ).
fof(f580,plain,
! [X1] :
( n0 != X1
| sP23(pull(agent6,trolley6),X1) ),
inference(equality_resolution,[],[f482]) ).
fof(f581,plain,
sP23(pull(agent6,trolley6),n0),
inference(equality_resolution,[],[f580]) ).
fof(f582,plain,
! [X1] :
( n0 != X1
| sP22(push(agent6,trolley6),X1) ),
inference(equality_resolution,[],[f485]) ).
fof(f583,plain,
sP22(push(agent6,trolley6),n0),
inference(equality_resolution,[],[f582]) ).
fof(f584,plain,
! [X1] :
( n0 != X1
| sP21(pull(agent7,trolley7),X1) ),
inference(equality_resolution,[],[f488]) ).
fof(f585,plain,
sP21(pull(agent7,trolley7),n0),
inference(equality_resolution,[],[f584]) ).
fof(f586,plain,
! [X1] :
( n0 != X1
| sP20(push(agent7,trolley7),X1) ),
inference(equality_resolution,[],[f491]) ).
fof(f587,plain,
sP20(push(agent7,trolley7),n0),
inference(equality_resolution,[],[f586]) ).
fof(f588,plain,
! [X1] :
( n0 != X1
| sP19(pull(agent8,trolley8),X1) ),
inference(equality_resolution,[],[f494]) ).
fof(f589,plain,
sP19(pull(agent8,trolley8),n0),
inference(equality_resolution,[],[f588]) ).
fof(f590,plain,
! [X1] :
( n0 != X1
| sP18(push(agent8,trolley8),X1) ),
inference(equality_resolution,[],[f497]) ).
fof(f591,plain,
sP18(push(agent8,trolley8),n0),
inference(equality_resolution,[],[f590]) ).
fof(f592,plain,
! [X1] :
( n0 != X1
| sP17(pull(agent9,trolley9),X1) ),
inference(equality_resolution,[],[f500]) ).
fof(f593,plain,
sP17(pull(agent9,trolley9),n0),
inference(equality_resolution,[],[f592]) ).
tcf(c_149,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(cnf_transformation,[],[f318]) ).
tcf(c_155,plain,
plus(n0,n1) = n1,
inference(cnf_transformation,[],[f324]) ).
tcf(c_200,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( initiates(X0,X3,X4)
| ~ sP6(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f370]) ).
tcf(c_254,plain,
! [X0: $i,X1: $i,X2: $i] :
( holdsAt(X1,plus(X2,n1))
| ~ happens(X0,X2)
| ~ initiates(X0,X1,X2) ),
inference(cnf_transformation,[],[f423]) ).
tcf(c_264,plain,
sP31(pull(agent1,trolley1),n0),
inference(cnf_transformation,[],[f561]) ).
tcf(c_265,plain,
sP31(push(agent1,trolley1),n0),
inference(cnf_transformation,[],[f563]) ).
tcf(c_266,plain,
sP31(pull(agent2,trolley2),n0),
inference(cnf_transformation,[],[f565]) ).
tcf(c_267,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP30(X0,X1) ),
inference(cnf_transformation,[],[f455]) ).
tcf(c_268,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP29(X0,X1) ),
inference(cnf_transformation,[],[f454]) ).
tcf(c_269,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP28(X0,X1) ),
inference(cnf_transformation,[],[f453]) ).
tcf(c_270,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP27(X0,X1) ),
inference(cnf_transformation,[],[f452]) ).
tcf(c_271,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP26(X0,X1) ),
inference(cnf_transformation,[],[f451]) ).
tcf(c_272,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP25(X0,X1) ),
inference(cnf_transformation,[],[f450]) ).
tcf(c_273,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP24(X0,X1) ),
inference(cnf_transformation,[],[f449]) ).
tcf(c_274,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP23(X0,X1) ),
inference(cnf_transformation,[],[f448]) ).
tcf(c_275,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP22(X0,X1) ),
inference(cnf_transformation,[],[f447]) ).
tcf(c_276,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP21(X0,X1) ),
inference(cnf_transformation,[],[f446]) ).
tcf(c_277,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP20(X0,X1) ),
inference(cnf_transformation,[],[f445]) ).
tcf(c_278,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP19(X0,X1) ),
inference(cnf_transformation,[],[f444]) ).
tcf(c_279,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP18(X0,X1) ),
inference(cnf_transformation,[],[f443]) ).
tcf(c_280,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP17(X0,X1) ),
inference(cnf_transformation,[],[f442]) ).
tcf(c_281,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP16(X0,X1) ),
inference(cnf_transformation,[],[f441]) ).
tcf(c_290,plain,
sP30(push(agent2,trolley2),n0),
inference(cnf_transformation,[],[f567]) ).
tcf(c_293,plain,
sP29(pull(agent3,trolley3),n0),
inference(cnf_transformation,[],[f569]) ).
tcf(c_296,plain,
sP28(push(agent3,trolley3),n0),
inference(cnf_transformation,[],[f571]) ).
tcf(c_299,plain,
sP27(pull(agent4,trolley4),n0),
inference(cnf_transformation,[],[f573]) ).
tcf(c_302,plain,
sP26(push(agent4,trolley4),n0),
inference(cnf_transformation,[],[f575]) ).
tcf(c_305,plain,
sP25(pull(agent5,trolley5),n0),
inference(cnf_transformation,[],[f577]) ).
tcf(c_308,plain,
sP24(push(agent5,trolley5),n0),
inference(cnf_transformation,[],[f579]) ).
tcf(c_311,plain,
sP23(pull(agent6,trolley6),n0),
inference(cnf_transformation,[],[f581]) ).
tcf(c_314,plain,
sP22(push(agent6,trolley6),n0),
inference(cnf_transformation,[],[f583]) ).
tcf(c_317,plain,
sP21(pull(agent7,trolley7),n0),
inference(cnf_transformation,[],[f585]) ).
tcf(c_320,plain,
sP20(push(agent7,trolley7),n0),
inference(cnf_transformation,[],[f587]) ).
tcf(c_323,plain,
sP19(pull(agent8,trolley8),n0),
inference(cnf_transformation,[],[f589]) ).
tcf(c_326,plain,
sP18(push(agent8,trolley8),n0),
inference(cnf_transformation,[],[f591]) ).
tcf(c_329,plain,
sP17(pull(agent9,trolley9),n0),
inference(cnf_transformation,[],[f593]) ).
tcf(c_335,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ~ sP31(X0,X1) ),
inference(cnf_transformation,[],[f505]) ).
tcf(c_550,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ~ sP31(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_335]) ).
tcf(c_726,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP30(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_267]) ).
tcf(c_732,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP29(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_268]) ).
tcf(c_738,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP28(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_269]) ).
tcf(c_744,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP27(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_270]) ).
tcf(c_750,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP26(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_271]) ).
tcf(c_756,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP25(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_272]) ).
tcf(c_762,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP24(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_273]) ).
tcf(c_768,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP23(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_274]) ).
tcf(c_774,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP22(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_275]) ).
tcf(c_780,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP21(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_276]) ).
tcf(c_786,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP20(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_277]) ).
tcf(c_792,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP19(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_278]) ).
tcf(c_798,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP18(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_279]) ).
tcf(c_804,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP17(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_280]) ).
tcf(c_810,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ~ sP16(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_281]) ).
tcf(c_4888,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ( X1 != n0 )
| ( push(agent2,trolley2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_726,c_290]) ).
tcf(c_4889,plain,
sP31(push(agent2,trolley2),n0),
inference(unflattening,[status(thm)],[c_4888]) ).
tcf(c_4965,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ( X1 != n0 )
| ( pull(agent3,trolley3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_732,c_293]) ).
tcf(c_4966,plain,
sP31(pull(agent3,trolley3),n0),
inference(unflattening,[status(thm)],[c_4965]) ).
tcf(c_5042,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ( X1 != n0 )
| ( push(agent3,trolley3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_738,c_296]) ).
tcf(c_5043,plain,
sP31(push(agent3,trolley3),n0),
inference(unflattening,[status(thm)],[c_5042]) ).
tcf(c_5119,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ( X1 != n0 )
| ( pull(agent4,trolley4) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_744,c_299]) ).
tcf(c_5120,plain,
sP31(pull(agent4,trolley4),n0),
inference(unflattening,[status(thm)],[c_5119]) ).
tcf(c_5196,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ( X1 != n0 )
| ( push(agent4,trolley4) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_750,c_302]) ).
tcf(c_5197,plain,
sP31(push(agent4,trolley4),n0),
inference(unflattening,[status(thm)],[c_5196]) ).
tcf(c_5273,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ( X1 != n0 )
| ( pull(agent5,trolley5) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_756,c_305]) ).
tcf(c_5274,plain,
sP31(pull(agent5,trolley5),n0),
inference(unflattening,[status(thm)],[c_5273]) ).
tcf(c_5350,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ( X1 != n0 )
| ( push(agent5,trolley5) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_762,c_308]) ).
tcf(c_5351,plain,
sP31(push(agent5,trolley5),n0),
inference(unflattening,[status(thm)],[c_5350]) ).
tcf(c_5427,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ( X1 != n0 )
| ( pull(agent6,trolley6) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_768,c_311]) ).
tcf(c_5428,plain,
sP31(pull(agent6,trolley6),n0),
inference(unflattening,[status(thm)],[c_5427]) ).
tcf(c_5504,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ( X1 != n0 )
| ( push(agent6,trolley6) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_774,c_314]) ).
tcf(c_5505,plain,
sP31(push(agent6,trolley6),n0),
inference(unflattening,[status(thm)],[c_5504]) ).
tcf(c_5581,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ( X1 != n0 )
| ( pull(agent7,trolley7) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_780,c_317]) ).
tcf(c_5582,plain,
sP31(pull(agent7,trolley7),n0),
inference(unflattening,[status(thm)],[c_5581]) ).
tcf(c_5658,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ( X1 != n0 )
| ( push(agent7,trolley7) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_786,c_320]) ).
tcf(c_5659,plain,
sP31(push(agent7,trolley7),n0),
inference(unflattening,[status(thm)],[c_5658]) ).
tcf(c_5735,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ( X1 != n0 )
| ( pull(agent8,trolley8) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_792,c_323]) ).
tcf(c_5736,plain,
sP31(pull(agent8,trolley8),n0),
inference(unflattening,[status(thm)],[c_5735]) ).
tcf(c_5812,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ( X1 != n0 )
| ( push(agent8,trolley8) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_798,c_326]) ).
tcf(c_5813,plain,
sP31(push(agent8,trolley8),n0),
inference(unflattening,[status(thm)],[c_5812]) ).
tcf(c_5889,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ( X1 != n0 )
| ( pull(agent9,trolley9) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_804,c_329]) ).
tcf(c_5890,plain,
sP31(pull(agent9,trolley9),n0),
inference(unflattening,[status(thm)],[c_5889]) ).
tcf(c_8235,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent1,trolley1) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_264,c_550]) ).
tcf(c_8236,plain,
happens(pull(agent1,trolley1),n0),
inference(unflattening,[status(thm)],[c_8235]) ).
tcf(c_8244,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent1,trolley1) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_265,c_550]) ).
tcf(c_8245,plain,
happens(push(agent1,trolley1),n0),
inference(unflattening,[status(thm)],[c_8244]) ).
tcf(c_8253,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent2,trolley2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_266,c_550]) ).
tcf(c_8254,plain,
happens(pull(agent2,trolley2),n0),
inference(unflattening,[status(thm)],[c_8253]) ).
tcf(c_8262,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent2,trolley2) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_550,c_4889]) ).
tcf(c_8263,plain,
happens(push(agent2,trolley2),n0),
inference(unflattening,[status(thm)],[c_8262]) ).
tcf(c_8271,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent3,trolley3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_550,c_4966]) ).
tcf(c_8272,plain,
happens(pull(agent3,trolley3),n0),
inference(unflattening,[status(thm)],[c_8271]) ).
tcf(c_8280,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent3,trolley3) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_550,c_5043]) ).
tcf(c_8281,plain,
happens(push(agent3,trolley3),n0),
inference(unflattening,[status(thm)],[c_8280]) ).
tcf(c_8289,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent4,trolley4) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_550,c_5120]) ).
tcf(c_8290,plain,
happens(pull(agent4,trolley4),n0),
inference(unflattening,[status(thm)],[c_8289]) ).
tcf(c_8298,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent4,trolley4) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_550,c_5197]) ).
tcf(c_8299,plain,
happens(push(agent4,trolley4),n0),
inference(unflattening,[status(thm)],[c_8298]) ).
tcf(c_8307,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent5,trolley5) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_550,c_5274]) ).
tcf(c_8308,plain,
happens(pull(agent5,trolley5),n0),
inference(unflattening,[status(thm)],[c_8307]) ).
tcf(c_8316,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent5,trolley5) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_550,c_5351]) ).
tcf(c_8317,plain,
happens(push(agent5,trolley5),n0),
inference(unflattening,[status(thm)],[c_8316]) ).
tcf(c_8325,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent6,trolley6) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_550,c_5428]) ).
tcf(c_8326,plain,
happens(pull(agent6,trolley6),n0),
inference(unflattening,[status(thm)],[c_8325]) ).
tcf(c_8334,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent6,trolley6) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_550,c_5505]) ).
tcf(c_8335,plain,
happens(push(agent6,trolley6),n0),
inference(unflattening,[status(thm)],[c_8334]) ).
tcf(c_8343,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent7,trolley7) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_550,c_5582]) ).
tcf(c_8344,plain,
happens(pull(agent7,trolley7),n0),
inference(unflattening,[status(thm)],[c_8343]) ).
tcf(c_8352,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent7,trolley7) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_550,c_5659]) ).
tcf(c_8353,plain,
happens(push(agent7,trolley7),n0),
inference(unflattening,[status(thm)],[c_8352]) ).
tcf(c_8361,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent8,trolley8) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_550,c_5736]) ).
tcf(c_8362,plain,
happens(pull(agent8,trolley8),n0),
inference(unflattening,[status(thm)],[c_8361]) ).
tcf(c_8370,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent8,trolley8) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_550,c_5813]) ).
tcf(c_8371,plain,
happens(push(agent8,trolley8),n0),
inference(unflattening,[status(thm)],[c_8370]) ).
tcf(c_8379,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( pull(agent9,trolley9) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_550,c_5890]) ).
tcf(c_8380,plain,
happens(pull(agent9,trolley9),n0),
inference(unflattening,[status(thm)],[c_8379]) ).
fof(f89,definition,
! [X0,X4,X3,X1,X2] :
( sP6(X0,X4,X3,X1,X2)
<=> ( happens(push(X3,X4),X2)
& X1 = spinning(X4)
& X0 = pull(X3,X4) ) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f90,definition,
! [X0,X4,X3,X1,X2] :
( sP7(X0,X4,X3,X1,X2)
<=> ( ~ happens(push(X3,X4),X2)
& X1 = backwards(X4)
& X0 = pull(X3,X4) ) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f91,plain,
! [X0,X1,X2] :
( initiates(X0,X1,X2)
<=> ? [X3,X4] :
( sP6(X0,X4,X3,X1,X2)
| sP7(X0,X4,X3,X1,X2)
| ( ~ happens(pull(X3,X4),X2)
& X1 = forwards(X4)
& X0 = push(X3,X4) ) ) ),
inference(definition_folding,[],[f45,f90,f89]) ).
fof(f102,definition,
! [X0,X1] :
( sP16(X0,X1)
<=> ( X1 = n0
& X0 = push(agent9,trolley9) ) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f103,definition,
! [X0,X1] :
( sP17(X0,X1)
<=> ( X1 = n0
& X0 = pull(agent9,trolley9) ) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f104,definition,
! [X0,X1] :
( sP18(X0,X1)
<=> ( X1 = n0
& X0 = push(agent8,trolley8) ) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f105,definition,
! [X0,X1] :
( sP19(X0,X1)
<=> ( X1 = n0
& X0 = pull(agent8,trolley8) ) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f106,definition,
! [X0,X1] :
( sP20(X0,X1)
<=> ( X1 = n0
& X0 = push(agent7,trolley7) ) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f107,definition,
! [X0,X1] :
( sP21(X0,X1)
<=> ( X1 = n0
& X0 = pull(agent7,trolley7) ) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f108,definition,
! [X0,X1] :
( sP22(X0,X1)
<=> ( X1 = n0
& X0 = push(agent6,trolley6) ) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f109,definition,
! [X0,X1] :
( sP23(X0,X1)
<=> ( X1 = n0
& X0 = pull(agent6,trolley6) ) ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f110,definition,
! [X0,X1] :
( sP24(X0,X1)
<=> ( X1 = n0
& X0 = push(agent5,trolley5) ) ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f111,definition,
! [X0,X1] :
( sP25(X0,X1)
<=> ( X1 = n0
& X0 = pull(agent5,trolley5) ) ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f112,definition,
! [X0,X1] :
( sP26(X0,X1)
<=> ( X1 = n0
& X0 = push(agent4,trolley4) ) ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f113,definition,
! [X0,X1] :
( sP27(X0,X1)
<=> ( X1 = n0
& X0 = pull(agent4,trolley4) ) ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f114,definition,
! [X0,X1] :
( sP28(X0,X1)
<=> ( X1 = n0
& X0 = push(agent3,trolley3) ) ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f115,definition,
! [X0,X1] :
( sP29(X0,X1)
<=> ( X1 = n0
& X0 = pull(agent3,trolley3) ) ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f116,definition,
! [X0,X1] :
( sP30(X0,X1)
<=> ( X1 = n0
& X0 = push(agent2,trolley2) ) ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f117,definition,
! [X0,X1] :
( sP31(X0,X1)
<=> ( sP16(X0,X1)
| sP17(X0,X1)
| sP18(X0,X1)
| sP19(X0,X1)
| sP20(X0,X1)
| sP21(X0,X1)
| sP22(X0,X1)
| sP23(X0,X1)
| sP24(X0,X1)
| sP25(X0,X1)
| sP26(X0,X1)
| sP27(X0,X1)
| sP28(X0,X1)
| sP29(X0,X1)
| sP30(X0,X1)
| ( X1 = n0
& X0 = pull(agent2,trolley2) )
| ( X1 = n0
& X0 = push(agent1,trolley1) )
| ( X1 = n0
& X0 = pull(agent1,trolley1) ) ) ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f118,plain,
! [X0,X1] :
( happens(X0,X1)
<=> sP31(X0,X1) ),
inference(definition_folding,[],[f48,f117,f116,f115,f114,f113,f112,f111,f110,f109,f108,f107,f106,f105,f104,f103,f102]) ).
fof(f142,plain,
! [X0,X4,X3,X1,X2] :
( ( ~ sP6(X0,X4,X3,X1,X2)
| ( happens(push(X3,X4),X2)
& X1 = spinning(X4)
& X0 = pull(X3,X4) ) )
& ( ~ happens(push(X3,X4),X2)
| spinning(X4) != X1
| pull(X3,X4) != X0
| sP6(X0,X4,X3,X1,X2) ) ),
inference(nnf_transformation,[],[f89]) ).
fof(f143,plain,
! [X0,X4,X3,X1,X2] :
( ( ~ sP6(X0,X4,X3,X1,X2)
| ( happens(push(X3,X4),X2)
& X1 = spinning(X4)
& X0 = pull(X3,X4) ) )
& ( ~ happens(push(X3,X4),X2)
| spinning(X4) != X1
| pull(X3,X4) != X0
| sP6(X0,X4,X3,X1,X2) ) ),
inference(flattening,[],[f142]) ).
fof(f144,plain,
! [X0,X1,X2,X3,X4] :
( ( ~ sP6(X0,X1,X2,X3,X4)
| ( happens(push(X2,X1),X4)
& spinning(X1) = X3
& pull(X2,X1) = X0 ) )
& ( ~ happens(push(X2,X1),X4)
| spinning(X1) != X3
| pull(X2,X1) != X0
| sP6(X0,X1,X2,X3,X4) ) ),
inference(rectify,[],[f143]) ).
fof(f209,plain,
! [X0,X1] :
( ( ~ sP16(X0,X1)
| ( X1 = n0
& X0 = push(agent9,trolley9) ) )
& ( n0 != X1
| push(agent9,trolley9) != X0
| sP16(X0,X1) ) ),
inference(nnf_transformation,[],[f102]) ).
fof(f210,plain,
! [X0,X1] :
( ( ~ sP16(X0,X1)
| ( X1 = n0
& X0 = push(agent9,trolley9) ) )
& ( n0 != X1
| push(agent9,trolley9) != X0
| sP16(X0,X1) ) ),
inference(flattening,[],[f209]) ).
fof(f366,plain,
! [X2,X3,X0,X1,X4] :
( ~ happens(push(X2,X1),X4)
| spinning(X1) != X3
| pull(X2,X1) != X0
| sP6(X0,X1,X2,X3,X4) ),
inference(cnf_transformation,[],[f144]) ).
fof(f503,plain,
! [X0,X1] :
( n0 != X1
| push(agent9,trolley9) != X0
| sP16(X0,X1) ),
inference(cnf_transformation,[],[f210]) ).
fof(f538,plain,
! [X2,X3,X1,X4] :
( ~ happens(push(X2,X1),X4)
| spinning(X1) != X3
| sP6(pull(X2,X1),X1,X2,X3,X4) ),
inference(equality_resolution,[],[f366]) ).
fof(f539,plain,
! [X2,X1,X4] :
( ~ happens(push(X2,X1),X4)
| sP6(pull(X2,X1),X1,X2,spinning(X1),X4) ),
inference(equality_resolution,[],[f538]) ).
fof(f594,plain,
! [X1] :
( n0 != X1
| sP16(push(agent9,trolley9),X1) ),
inference(equality_resolution,[],[f503]) ).
fof(f595,plain,
sP16(push(agent9,trolley9),n0),
inference(equality_resolution,[],[f594]) ).
tcf(c_194,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP6(pull(X0,X1),X1,X0,spinning(X1),X2)
| ~ happens(push(X0,X1),X2) ),
inference(cnf_transformation,[],[f539]) ).
tcf(c_332,plain,
sP16(push(agent9,trolley9),n0),
inference(cnf_transformation,[],[f595]) ).
tcf(c_5965,plain,
! [X0: $i,X1: $i] :
( sP31(X0,X1)
| ( X1 != n0 )
| ( push(agent9,trolley9) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_810,c_332]) ).
tcf(c_5966,plain,
sP31(push(agent9,trolley9),n0),
inference(unflattening,[status(thm)],[c_5965]) ).
tcf(c_8388,plain,
! [X0: $i,X1: $i] :
( happens(X0,X1)
| ( X1 != n0 )
| ( push(agent9,trolley9) != X0 ) ),
inference(resolution_lifted,[status(thm)],[c_550,c_5966]) ).
tcf(c_8389,plain,
happens(push(agent9,trolley9),n0),
inference(unflattening,[status(thm)],[c_8388]) ).
tcf(c_20466,plain,
! [X0: $i,X1: $i,X2: $i] :
( initiates(pull(X0,X1),spinning(X1),X2)
| ~ happens(push(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_194,c_200]) ).
tcf(c_20495,plain,
! [X0: $i,X1: $i,X2: $i] :
( holdsAt(spinning(X1),plus(X2,n1))
| ~ happens(pull(X0,X1),X2)
| ~ happens(push(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_20466,c_254]) ).
tcf(c_21276,plain,
( holdsAt(spinning(trolley1),plus(n0,n1))
| ~ happens(pull(agent1,trolley1),n0) ),
inference(superposition,[status(thm)],[c_8245,c_20495]) ).
tcf(c_21277,plain,
( holdsAt(spinning(trolley2),plus(n0,n1))
| ~ happens(pull(agent2,trolley2),n0) ),
inference(superposition,[status(thm)],[c_8263,c_20495]) ).
tcf(c_21278,plain,
( holdsAt(spinning(trolley3),plus(n0,n1))
| ~ happens(pull(agent3,trolley3),n0) ),
inference(superposition,[status(thm)],[c_8281,c_20495]) ).
tcf(c_21279,plain,
( holdsAt(spinning(trolley4),plus(n0,n1))
| ~ happens(pull(agent4,trolley4),n0) ),
inference(superposition,[status(thm)],[c_8299,c_20495]) ).
tcf(c_21280,plain,
( holdsAt(spinning(trolley5),plus(n0,n1))
| ~ happens(pull(agent5,trolley5),n0) ),
inference(superposition,[status(thm)],[c_8317,c_20495]) ).
tcf(c_21281,plain,
( holdsAt(spinning(trolley6),plus(n0,n1))
| ~ happens(pull(agent6,trolley6),n0) ),
inference(superposition,[status(thm)],[c_8335,c_20495]) ).
tcf(c_21282,plain,
( holdsAt(spinning(trolley7),plus(n0,n1))
| ~ happens(pull(agent7,trolley7),n0) ),
inference(superposition,[status(thm)],[c_8353,c_20495]) ).
tcf(c_21283,plain,
( holdsAt(spinning(trolley8),plus(n0,n1))
| ~ happens(pull(agent8,trolley8),n0) ),
inference(superposition,[status(thm)],[c_8371,c_20495]) ).
tcf(c_21284,plain,
( holdsAt(spinning(trolley9),plus(n0,n1))
| ~ happens(pull(agent9,trolley9),n0) ),
inference(superposition,[status(thm)],[c_8389,c_20495]) ).
tcf(c_21285,plain,
( holdsAt(spinning(trolley9),n1)
| ~ happens(pull(agent9,trolley9),n0) ),
inference(light_normalisation,[status(thm)],[c_21284,c_155]) ).
tcf(c_21286,plain,
holdsAt(spinning(trolley9),n1),
inference(forward_subsumption_resolution,[status(thm)],[c_21285,c_8380]) ).
tcf(c_21287,plain,
( holdsAt(spinning(trolley8),n1)
| ~ happens(pull(agent8,trolley8),n0) ),
inference(light_normalisation,[status(thm)],[c_21283,c_155]) ).
tcf(c_21288,plain,
holdsAt(spinning(trolley8),n1),
inference(forward_subsumption_resolution,[status(thm)],[c_21287,c_8362]) ).
tcf(c_21289,plain,
( holdsAt(spinning(trolley7),n1)
| ~ happens(pull(agent7,trolley7),n0) ),
inference(light_normalisation,[status(thm)],[c_21282,c_155]) ).
tcf(c_21290,plain,
holdsAt(spinning(trolley7),n1),
inference(forward_subsumption_resolution,[status(thm)],[c_21289,c_8344]) ).
tcf(c_21291,plain,
( holdsAt(spinning(trolley6),n1)
| ~ happens(pull(agent6,trolley6),n0) ),
inference(light_normalisation,[status(thm)],[c_21281,c_155]) ).
tcf(c_21292,plain,
holdsAt(spinning(trolley6),n1),
inference(forward_subsumption_resolution,[status(thm)],[c_21291,c_8326]) ).
tcf(c_21293,plain,
( holdsAt(spinning(trolley5),n1)
| ~ happens(pull(agent5,trolley5),n0) ),
inference(light_normalisation,[status(thm)],[c_21280,c_155]) ).
tcf(c_21294,plain,
holdsAt(spinning(trolley5),n1),
inference(forward_subsumption_resolution,[status(thm)],[c_21293,c_8308]) ).
tcf(c_21295,plain,
( holdsAt(spinning(trolley4),n1)
| ~ happens(pull(agent4,trolley4),n0) ),
inference(light_normalisation,[status(thm)],[c_21279,c_155]) ).
tcf(c_21296,plain,
holdsAt(spinning(trolley4),n1),
inference(forward_subsumption_resolution,[status(thm)],[c_21295,c_8290]) ).
tcf(c_21297,plain,
( holdsAt(spinning(trolley3),n1)
| ~ happens(pull(agent3,trolley3),n0) ),
inference(light_normalisation,[status(thm)],[c_21278,c_155]) ).
tcf(c_21298,plain,
holdsAt(spinning(trolley3),n1),
inference(forward_subsumption_resolution,[status(thm)],[c_21297,c_8272]) ).
tcf(c_21299,plain,
( holdsAt(spinning(trolley2),n1)
| ~ happens(pull(agent2,trolley2),n0) ),
inference(light_normalisation,[status(thm)],[c_21277,c_155]) ).
tcf(c_21300,plain,
holdsAt(spinning(trolley2),n1),
inference(forward_subsumption_resolution,[status(thm)],[c_21299,c_8254]) ).
tcf(c_21301,plain,
( holdsAt(spinning(trolley1),n1)
| ~ happens(pull(agent1,trolley1),n0) ),
inference(light_normalisation,[status(thm)],[c_21276,c_155]) ).
tcf(c_21302,plain,
holdsAt(spinning(trolley1),n1),
inference(forward_subsumption_resolution,[status(thm)],[c_21301,c_8236]) ).
tcf(c_21309,plain,
( ~ 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(backward_subsumption_resolution,[status(thm)],[c_149,c_21286]) ).
tcf(c_21310,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_21309,c_21288,c_21290,c_21292,c_21294,c_21296,c_21298,c_21300,c_21302]) ).
%------------------------------------------------------------------------------
%----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_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.07/0.34 % Computer : n019.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Fri Sep 25 08:07:48 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.38 Running first-order theorem proving
% 0.12/0.38 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.40
% 0.12/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.40
% 0.12/0.40 % Detected problem language: tptp
% 0.12/0.41 % Proving...
% 6.90/2.14 % SZS status Started for theBenchmark.p
% 6.90/2.14 % SZS status Theorem for theBenchmark.p
% 6.90/2.14
% 6.90/2.14 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.90/2.14
% 6.90/2.14 % ------ iProver source info
% 6.90/2.14
% 6.90/2.14 % git: date: 2026-07-19 20:42:38 +0200
% 6.90/2.14 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.90/2.14 % git: non_committed_changes: false
% 6.90/2.14
% 6.90/2.14 % ------ Parsing...
% 6.90/2.14 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.90/2.14
% 6.90/2.14 % ------ Preprocessing... sup_sim: 0 sf_s rm: 2 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe_e sup_sim: 0 sf_s rm: 20 0s sf_e pe_s pe_e %
% 6.90/2.14
% 6.90/2.14 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 6.90/2.14
% 6.90/2.14 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 6.90/2.14 % ------ Proving...
% 6.90/2.14 % ------ Problem Properties
% 6.90/2.14
% 6.90/2.14 %
% 6.90/2.14 % clauses 239
% 6.90/2.14 % conjectures 1
% 6.90/2.14 % EPR 103
% 6.90/2.14 % Horn 207
% 6.90/2.14 % unary 133
% 6.90/2.14 % binary 78
% 6.90/2.14 % lits 419
% 6.90/2.14 % lits eq 151
% 6.90/2.14 % fd_pure 0
% 6.90/2.14 % fd_pseudo 0
% 6.90/2.14 % fd_cond 5
% 6.90/2.14 % fd_pseudo_cond 31
% 6.90/2.14 % AC symbols 0
% 6.90/2.14
% 6.90/2.14 % ------ Schedule dynamic 5 is on
% 6.90/2.14
% 6.90/2.14 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 6.90/2.14
% 6.90/2.14
% 6.90/2.14 % ------
% 6.90/2.14 % Current options:
% 6.90/2.14 % ------
% 6.90/2.14
% 6.90/2.14
% 6.90/2.14 %
% 6.90/2.14
% 6.90/2.14 % ------ Proving...
% 6.90/2.14 %
% 6.90/2.14
% 6.90/2.14 % SZS status Theorem for theBenchmark.p
% 6.90/2.14
% 6.90/2.14 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 11.28/2.15
% 11.28/2.15
%------------------------------------------------------------------------------