%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : SYO632-1 : TPTP v9.3.1. Released v7.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Wed Oct 7 11:08:54 AM UTC 2026
% Result : Unsatisfiable 0.08s 0.24s
% Output : CNFRefutation 0.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO632-1 : TPTP v9.3.1. Released v7.1.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.18 % Computer : n019.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Oct 6 17:44:16 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox/solver/bin/eprover /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.24
% 0.08/0.24 No.of.Axioms: 5
% 0.08/0.24
% 0.08/0.24 Length.of.Defs: 0
% 0.08/0.24
% 0.08/0.24 Contains.Choice.Funs: false
% 0.08/0.24 eprover: <stdin>:1:(Column 63):(just read ''LEQ''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 0.08/0.24 .eprover: <stdin>:1:(Column 63):(just read ''LEQ''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 0.08/0.24 eprover: <stdin>:1:(Column 63):(just read ''LEQ''): Closing bracket (')') expected, but String enclosed in single quote ('') read
% 0.08/0.24
% 0.08/0.24
% 0.08/0.24 ********************************
% 0.08/0.24 * All subproblems solved! *
% 0.08/0.24 ********************************
% 0.08/0.24 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:5,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:true,expand_extuni:false,foatp:e,atp_timeout:74,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:78,loop_count:6,foatp_calls:3,translation:fof_full)
% 0.08/0.24
% 0.08/0.24 %**** Beginning of derivation protocol ****
% 0.08/0.24 % SZS output start CNFRefutation
% 0.08/0.24 thf(tp_'0',type,('0': $i)).
% 0.08/0.24 thf(tp_'AP',type,('AP': ($i>($i>$i)))).
% 0.08/0.24 thf(tp_'E',type,('E': ($i>($i>$o)))).
% 0.08/0.24 thf(tp_'LEQ',type,('LEQ': ($i>($i>$o)))).
% 0.08/0.24 thf(tp_f,type,(f: ($i>$i))).
% 0.08/0.24 thf(tp_s,type,(s: ($i>$i))).
% 0.08/0.24 thf(2,axiom,(![A_0:$i,B_0:$i]: ((~ (('E'@(f@A_0))@'0')) | (~ (('E'@(f@B_0))@(s@'0'))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_1_04)).
% 0.08/0.24 thf(3,axiom,(![B:$i]: (('E'@(f@B))@(s@'0'))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_0_03)).
% 0.08/0.24 thf(4,axiom,(![K:$i]: (('E'@(f@(('AP'@(s@(s@'0')))@K)))@'0')),file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2_02)).
% 0.08/0.24 thf(10,plain,(((![A_0:$i,B_0:$i]: ((~ (('E'@(f@A_0))@'0')) | (~ (('E'@(f@B_0))@(s@'0')))))=$true)),inference(unfold_def,[status(thm)],[2])).
% 0.08/0.24 thf(11,plain,(((![B:$i]: (('E'@(f@B))@(s@'0')))=$true)),inference(unfold_def,[status(thm)],[3])).
% 0.08/0.24 thf(12,plain,(((![K:$i]: (('E'@(f@(('AP'@(s@(s@'0')))@K)))@'0'))=$true)),inference(unfold_def,[status(thm)],[4])).
% 0.08/0.24 thf(15,plain,((((![A_0:$i]: (~ (('E'@(f@A_0))@'0'))) | (![B_0:$i]: (~ (('E'@(f@B_0))@(s@'0')))))=$true)),inference(extcnf_combined,[status(esa)],[10])).
% 0.08/0.24 thf(17,plain,(((![K:$i]: (('E'@(f@(('AP'@(s@(s@'0')))@K)))@'0'))=$true)),inference(copy,[status(thm)],[12])).
% 0.08/0.24 thf(18,plain,(((![B:$i]: (('E'@(f@B))@(s@'0')))=$true)),inference(copy,[status(thm)],[11])).
% 0.08/0.24 thf(19,plain,((((![A_0:$i]: (~ (('E'@(f@A_0))@'0'))) | (![B_0:$i]: (~ (('E'@(f@B_0))@(s@'0')))))=$true)),inference(copy,[status(thm)],[15])).
% 0.08/0.24 thf(23,plain,(![SV2:$i]: (((('E'@(f@(('AP'@(s@(s@'0')))@SV2)))@'0')=$true))),inference(extcnf_forall_pos,[status(thm)],[17])).
% 0.08/0.24 thf(24,plain,(![SV3:$i]: (((('E'@(f@SV3))@(s@'0'))=$true))),inference(extcnf_forall_pos,[status(thm)],[18])).
% 0.08/0.24 thf(25,plain,(((![A_0:$i]: (~ (('E'@(f@A_0))@'0')))=$true) | ((![B_0:$i]: (~ (('E'@(f@B_0))@(s@'0'))))=$true)),inference(extcnf_or_pos,[status(thm)],[19])).
% 0.08/0.24 thf(28,plain,(![SV5:$i]: (((~ (('E'@(f@SV5))@'0'))=$true) | ((![B_0:$i]: (~ (('E'@(f@B_0))@(s@'0'))))=$true))),inference(extcnf_forall_pos,[status(thm)],[25])).
% 0.08/0.24 thf(30,plain,(![SV5:$i]: (((('E'@(f@SV5))@'0')=$false) | ((![B_0:$i]: (~ (('E'@(f@B_0))@(s@'0'))))=$true))),inference(extcnf_not_pos,[status(thm)],[28])).
% 0.08/0.24 thf(31,plain,(![SV5:$i,SV7:$i]: (((~ (('E'@(f@SV7))@(s@'0')))=$true) | ((('E'@(f@SV5))@'0')=$false))),inference(extcnf_forall_pos,[status(thm)],[30])).
% 0.08/0.24 thf(32,plain,(![SV5:$i,SV7:$i]: (((('E'@(f@SV7))@(s@'0'))=$false) | ((('E'@(f@SV5))@'0')=$false))),inference(extcnf_not_pos,[status(thm)],[31])).
% 0.08/0.24 thf(48,plain,(![SV9:$i]: (((('E'@(f@(('AP'@(s@(s@'0')))@SV9)))@'0')=$true))),inference(rename,[status(thm)],[23])).
% 0.08/0.24 thf(49,plain,(![SV10:$i]: (((('E'@(f@SV10))@(s@'0'))=$true))),inference(rename,[status(thm)],[24])).
% 0.08/0.24 thf(51,plain,(![SV13:$i,SV14:$i]: (((('E'@(f@SV14))@(s@'0'))=$false) | ((('E'@(f@SV13))@'0')=$false))),inference(rename,[status(thm)],[32])).
% 0.08/0.24 thf(56,plain,(![SV13:$i,SV14:$i,SV9:$i]: ((((('E'@(f@SV13))@'0') = (('E'@(f@(('AP'@(s@(s@'0')))@SV9)))@'0'))=$false) | ((('E'@(f@SV14))@(s@'0'))=$false))),inference(res,[status(thm)],[51,48])).
% 0.08/0.24 thf(63,plain,(![SV14:$i]: (((('E'@(f@SV14))@(s@'0'))=$false))),inference(extuni,[status(esa)],[56:[bind(SV13,$thf(('AP'@(s@(s@'0')))@SV9))]])).
% 0.08/0.24 thf(71,plain,(![SV15:$i]: (((('E'@(f@SV15))@(s@'0'))=$false))),inference(rename,[status(thm)],[63])).
% 0.08/0.24 thf(73,plain,(![SV15:$i,SV10:$i]: ((((('E'@(f@SV15))@(s@'0')) = (('E'@(f@SV10))@(s@'0')))=$false))),inference(res,[status(thm)],[71,49])).
% 0.08/0.24 thf(78,plain,((($false)=$true)),inference(extuni,[status(esa)],[73:[bind(SV15,$thf(SV10))]])).
% 0.08/0.24 thf(79,plain,($false),inference(solved_all_splits,[solved_all_splits(join,[])],[78])).
% 0.08/0.24 % SZS output end CNFRefutation
% 0.08/0.24
% 0.08/0.24 %**** End of derivation protocol ****
% 0.08/0.24 %**** no. of clauses in derivation: 26 ****
% 0.08/0.24 %**** clause counter: 78 ****
% 0.08/0.24
% 0.08/0.24 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : (rf:0,axioms:5,ps:3,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:true,expand_extuni:false,foatp:e,atp_timeout:74,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:78,loop_count:6,foatp_calls:3,translation:fof_full)
%------------------------------------------------------------------------------