%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SYN364+1 : TPTP v8.1.0. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Thu Jul 21 08:17:46 EDT 2022
% Result : Theorem 0.33s 1.41s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN364+1 : TPTP v8.1.0. Released v2.0.0.
% 0.03/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n019.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Tue Jul 12 06:52:08 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.33/1.41 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.42 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.42
% 0.33/1.42 %-----------------------------------------------------
% 0.33/1.42 fof(x2115, conjecture, ! [_7689] : (? [_7697] : big_p(_7689, _7697) => ! [_7715] : big_p(_7715, _7715)) & ! [_7733] : ? [_7741] : (big_p(_7733, _7741) | big_m(_7733) & big_q(f(_7733, _7741))) & ! [_7780] : (big_q(_7780) => ~ big_m(g(_7780))) => ! [_7733] : ? [_7741] : (big_p(g(_7733), _7741) & big_p(_7733, _7733)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', x2115)).
% 0.33/1.42
% 0.33/1.42 cnf(1, plain, [big_p(g(2 ^ []), _4690), big_p(2 ^ [], 2 ^ [])], clausify(x2115)).
% 0.33/1.42 cnf(2, plain, [big_p(_3303, _3364), -(big_p(_3458, _3458))], clausify(x2115)).
% 0.33/1.42 cnf(3, plain, [-(big_p(_3584, 1 ^ [_3584])), -(big_m(_3584))], clausify(x2115)).
% 0.33/1.42 cnf(4, plain, [-(big_p(_3584, 1 ^ [_3584])), -(big_q(f(_3584, 1 ^ [_3584])))], clausify(x2115)).
% 0.33/1.42 cnf(5, plain, [big_q(_3894), big_m(g(_3894))], clausify(x2115)).
% 0.33/1.42
% 0.33/1.42 cnf('1',plain,[big_q(f(g(2 ^ []), 1 ^ [g(2 ^ [])])), big_m(g(f(g(2 ^ []), 1 ^ [g(2 ^ [])])))],start(5,bind([[_3894], [f(g(2 ^ []), 1 ^ [g(2 ^ [])])]]))).
% 0.33/1.42 cnf('1.1',plain,[-(big_q(f(g(2 ^ []), 1 ^ [g(2 ^ [])]))), -(big_p(g(2 ^ []), 1 ^ [g(2 ^ [])]))],extension(4,bind([[_3584], [g(2 ^ [])]]))).
% 0.33/1.42 cnf('1.1.1',plain,[big_p(g(2 ^ []), 1 ^ [g(2 ^ [])]), big_p(2 ^ [], 2 ^ [])],extension(1,bind([[_4690], [1 ^ [g(2 ^ [])]]]))).
% 0.33/1.42 cnf('1.1.1.1',plain,[-(big_p(2 ^ [], 2 ^ [])), big_p(g(2 ^ []), 1 ^ [g(2 ^ [])])],extension(2,bind([[_3458, _3303, _3364], [2 ^ [], g(2 ^ []), 1 ^ [g(2 ^ [])]]]))).
% 0.33/1.42 cnf('1.1.1.1.1',plain,[-(big_p(g(2 ^ []), 1 ^ [g(2 ^ [])]))],reduction('1.1')).
% 0.33/1.42 cnf('1.2',plain,[-(big_m(g(f(g(2 ^ []), 1 ^ [g(2 ^ [])])))), -(big_p(g(f(g(2 ^ []), 1 ^ [g(2 ^ [])])), 1 ^ [g(f(g(2 ^ []), 1 ^ [g(2 ^ [])]))]))],extension(3,bind([[_3584], [g(f(g(2 ^ []), 1 ^ [g(2 ^ [])]))]]))).
% 0.33/1.42 cnf('1.2.1',plain,[big_p(g(f(g(2 ^ []), 1 ^ [g(2 ^ [])])), 1 ^ [g(f(g(2 ^ []), 1 ^ [g(2 ^ [])]))]), -(big_p(g(2 ^ []), g(2 ^ [])))],extension(2,bind([[_3303, _3364, _3458], [g(f(g(2 ^ []), 1 ^ [g(2 ^ [])])), 1 ^ [g(f(g(2 ^ []), 1 ^ [g(2 ^ [])]))], g(2 ^ [])]]))).
% 0.33/1.42 cnf('1.2.1.1',plain,[big_p(g(2 ^ []), g(2 ^ [])), big_p(2 ^ [], 2 ^ [])],extension(1,bind([[_4690], [g(2 ^ [])]]))).
% 0.33/1.42 cnf('1.2.1.1.1',plain,[-(big_p(2 ^ [], 2 ^ [])), big_p(g(2 ^ []), g(2 ^ []))],extension(2,bind([[_3458, _3303, _3364], [2 ^ [], g(2 ^ []), g(2 ^ [])]]))).
% 0.33/1.42 cnf('1.2.1.1.1.1',plain,[-(big_p(g(2 ^ []), g(2 ^ [])))],reduction('1.2.1')).
% 0.33/1.42 %-----------------------------------------------------
% 0.33/1.43
% 0.33/1.43 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------