%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWV399+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n023.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 : Wed Jul 20 19:50:44 EDT 2022
% Result : Theorem 0.83s 1.40s
% Output : Proof 0.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWV399+1 : TPTP v8.1.0. Released v3.3.0.
% 0.00/0.11 % Command : leancop_casc.sh %s %d
% 0.10/0.33 % Computer : n023.cluster.edu
% 0.10/0.33 % Model : x86_64 x86_64
% 0.10/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.33 % Memory : 8042.1875MB
% 0.10/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.33 % CPULimit : 300
% 0.10/0.33 % WCLimit : 600
% 0.10/0.33 % DateTime : Wed Jun 15 18:35:50 EDT 2022
% 0.10/0.33 % CPUTime :
% 0.83/1.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.83/1.41 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.83/1.41
% 0.83/1.41 %-----------------------------------------------------
% 0.83/1.41 fof(l35_co, conjecture, ! [_50142] : (? [_50150, _50153] : (pair_in_list(_50142, _50150, _50153) & strictly_less_than(_50150, _50153)) => ! [_50184] : ? [_50192, _50195] : (pair_in_list(update_slb(_50142, _50184), _50192, _50195) & strictly_less_than(_50192, _50195))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l35_co)).
% 0.83/1.41 fof(transitivity, axiom, ! [_50497, _50500, _50503] : (less_than(_50497, _50500) & less_than(_50500, _50503) => less_than(_50497, _50503)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV007+0.ax', transitivity)).
% 0.83/1.41 fof(totality, axiom, ! [_50682, _50685] : (less_than(_50682, _50685) | less_than(_50685, _50682)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV007+0.ax', totality)).
% 0.83/1.41 fof(stricly_smaller_definition, axiom, ! [_50831, _50834] : (strictly_less_than(_50831, _50834) <=> less_than(_50831, _50834) & ~ less_than(_50834, _50831)), file('/export/starexec/sandbox2/benchmark/Axioms/SWV007+0.ax', stricly_smaller_definition)).
% 0.83/1.41 fof(l35_li3637, lemma, ! [_51024, _51027, _51030, _51033] : (pair_in_list(_51024, _51027, _51030) & less_than(_51033, _51030) => pair_in_list(update_slb(_51024, _51033), _51027, _51030)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l35_li3637)).
% 0.83/1.41 fof(l35_li3839, lemma, ! [_51250, _51253, _51256, _51259] : (pair_in_list(_51250, _51253, _51256) & strictly_less_than(_51256, _51259) => pair_in_list(update_slb(_51250, _51259), _51253, _51259)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', l35_li3839)).
% 0.83/1.41
% 0.83/1.41 cnf(1, plain, [-(pair_in_list(1 ^ [], 2 ^ [], 3 ^ []))], clausify(l35_co)).
% 0.83/1.41 cnf(2, plain, [-(strictly_less_than(2 ^ [], 3 ^ []))], clausify(l35_co)).
% 0.83/1.41 cnf(3, plain, [pair_in_list(update_slb(1 ^ [], 4 ^ []), _34150, _34155), strictly_less_than(_34150, _34155)], clausify(l35_co)).
% 0.83/1.41 cnf(4, plain, [-(less_than(_19444, _19555)), less_than(_19444, _19500), less_than(_19500, _19555)], clausify(transitivity)).
% 0.83/1.41 cnf(5, plain, [-(less_than(_19911, _19956)), -(less_than(_19956, _19911))], clausify(totality)).
% 0.83/1.41 cnf(6, plain, [strictly_less_than(_20395, _20448), less_than(_20448, _20395)], clausify(stricly_smaller_definition)).
% 0.83/1.41 cnf(7, plain, [-(strictly_less_than(_20395, _20448)), less_than(_20395, _20448), -(less_than(_20448, _20395))], clausify(stricly_smaller_definition)).
% 0.83/1.41 cnf(8, plain, [-(pair_in_list(update_slb(_27925, _28120), _27991, _28056)), pair_in_list(_27925, _27991, _28056), less_than(_28120, _28056)], clausify(l35_li3637)).
% 0.83/1.41 cnf(9, plain, [-(pair_in_list(update_slb(_28599, _28794), _28665, _28794)), pair_in_list(_28599, _28665, _28730), strictly_less_than(_28730, _28794)], clausify(l35_li3839)).
% 0.83/1.41
% 0.83/1.41 cnf('1',plain,[pair_in_list(update_slb(1 ^ [], 4 ^ []), 2 ^ [], 4 ^ []), strictly_less_than(2 ^ [], 4 ^ [])],start(3,bind([[_34150, _34155], [2 ^ [], 4 ^ []]]))).
% 0.83/1.41 cnf('1.1',plain,[-(pair_in_list(update_slb(1 ^ [], 4 ^ []), 2 ^ [], 4 ^ [])), pair_in_list(1 ^ [], 2 ^ [], 3 ^ []), strictly_less_than(3 ^ [], 4 ^ [])],extension(9,bind([[_28599, _28665, _28730, _28794], [1 ^ [], 2 ^ [], 3 ^ [], 4 ^ []]]))).
% 0.83/1.41 cnf('1.1.1',plain,[-(pair_in_list(1 ^ [], 2 ^ [], 3 ^ []))],extension(1)).
% 0.83/1.41 cnf('1.1.2',plain,[-(strictly_less_than(3 ^ [], 4 ^ [])), less_than(3 ^ [], 4 ^ []), -(less_than(4 ^ [], 3 ^ []))],extension(7,bind([[_20448, _20395], [4 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.1.2.1',plain,[-(less_than(3 ^ [], 4 ^ [])), -(less_than(4 ^ [], 3 ^ []))],extension(5,bind([[_19956, _19911], [4 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.1.2.1.1',plain,[less_than(4 ^ [], 3 ^ []), -(pair_in_list(update_slb(1 ^ [], 4 ^ []), 2 ^ [], 3 ^ [])), pair_in_list(1 ^ [], 2 ^ [], 3 ^ [])],extension(8,bind([[_28120, _27925, _27991, _28056], [4 ^ [], 1 ^ [], 2 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.1.2.1.1.1',plain,[pair_in_list(update_slb(1 ^ [], 4 ^ []), 2 ^ [], 3 ^ []), strictly_less_than(2 ^ [], 3 ^ [])],extension(3,bind([[_34150, _34155], [2 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.1.2.1.1.1.1',plain,[-(strictly_less_than(2 ^ [], 3 ^ []))],extension(2)).
% 0.83/1.41 cnf('1.1.2.1.1.2',plain,[-(pair_in_list(1 ^ [], 2 ^ [], 3 ^ []))],extension(1)).
% 0.83/1.41 cnf('1.1.2.2',plain,[less_than(4 ^ [], 3 ^ []), -(less_than(4 ^ [], 3 ^ [])), less_than(4 ^ [], 4 ^ [])],extension(4,bind([[_19555, _19444, _19500], [3 ^ [], 4 ^ [], 4 ^ []]]))).
% 0.83/1.41 cnf('1.1.2.2.1',plain,[less_than(4 ^ [], 3 ^ []), -(pair_in_list(update_slb(1 ^ [], 4 ^ []), 2 ^ [], 3 ^ [])), pair_in_list(1 ^ [], 2 ^ [], 3 ^ [])],extension(8,bind([[_28120, _27925, _27991, _28056], [4 ^ [], 1 ^ [], 2 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.1.2.2.1.1',plain,[pair_in_list(update_slb(1 ^ [], 4 ^ []), 2 ^ [], 3 ^ []), strictly_less_than(2 ^ [], 3 ^ [])],extension(3,bind([[_34150, _34155], [2 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.1.2.2.1.1.1',plain,[-(strictly_less_than(2 ^ [], 3 ^ []))],extension(2)).
% 0.83/1.41 cnf('1.1.2.2.1.2',plain,[-(pair_in_list(1 ^ [], 2 ^ [], 3 ^ []))],extension(1)).
% 0.83/1.41 cnf('1.1.2.2.2',plain,[-(less_than(4 ^ [], 4 ^ [])), less_than(4 ^ [], 3 ^ []), less_than(3 ^ [], 4 ^ [])],extension(4,bind([[_19444, _19500, _19555], [4 ^ [], 3 ^ [], 4 ^ []]]))).
% 0.83/1.41 cnf('1.1.2.2.2.1',plain,[-(less_than(4 ^ [], 3 ^ []))],reduction('1.1.2')).
% 0.83/1.41 cnf('1.1.2.2.2.2',plain,[-(less_than(3 ^ [], 4 ^ []))],lemmata('1.1.2')).
% 0.83/1.41 cnf('1.2',plain,[-(strictly_less_than(2 ^ [], 4 ^ [])), less_than(2 ^ [], 4 ^ []), -(less_than(4 ^ [], 2 ^ []))],extension(7,bind([[_20448, _20395], [4 ^ [], 2 ^ []]]))).
% 0.83/1.41 cnf('1.2.1',plain,[-(less_than(2 ^ [], 4 ^ [])), -(less_than(4 ^ [], 2 ^ []))],extension(5,bind([[_19956, _19911], [4 ^ [], 2 ^ []]]))).
% 0.83/1.41 cnf('1.2.1.1',plain,[less_than(4 ^ [], 2 ^ []), -(less_than(4 ^ [], 3 ^ [])), less_than(2 ^ [], 3 ^ [])],extension(4,bind([[_19444, _19500, _19555], [4 ^ [], 2 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.2.1.1.1',plain,[less_than(4 ^ [], 3 ^ []), -(pair_in_list(update_slb(1 ^ [], 4 ^ []), 2 ^ [], 3 ^ [])), pair_in_list(1 ^ [], 2 ^ [], 3 ^ [])],extension(8,bind([[_28120, _27925, _27991, _28056], [4 ^ [], 1 ^ [], 2 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.2.1.1.1.1',plain,[pair_in_list(update_slb(1 ^ [], 4 ^ []), 2 ^ [], 3 ^ []), strictly_less_than(2 ^ [], 3 ^ [])],extension(3,bind([[_34150, _34155], [2 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.2.1.1.1.1.1',plain,[-(strictly_less_than(2 ^ [], 3 ^ []))],extension(2)).
% 0.83/1.41 cnf('1.2.1.1.1.2',plain,[-(pair_in_list(1 ^ [], 2 ^ [], 3 ^ []))],extension(1)).
% 0.83/1.41 cnf('1.2.1.1.2',plain,[-(less_than(2 ^ [], 3 ^ [])), -(less_than(3 ^ [], 2 ^ []))],extension(5,bind([[_19956, _19911], [3 ^ [], 2 ^ []]]))).
% 0.83/1.41 cnf('1.2.1.1.2.1',plain,[less_than(3 ^ [], 2 ^ []), strictly_less_than(2 ^ [], 3 ^ [])],extension(6,bind([[_20395, _20448], [2 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.2.1.1.2.1.1',plain,[-(strictly_less_than(2 ^ [], 3 ^ []))],extension(2)).
% 0.83/1.41 cnf('1.2.2',plain,[less_than(4 ^ [], 2 ^ []), -(less_than(4 ^ [], 3 ^ [])), less_than(2 ^ [], 3 ^ [])],extension(4,bind([[_19444, _19500, _19555], [4 ^ [], 2 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.2.2.1',plain,[less_than(4 ^ [], 3 ^ []), -(less_than(4 ^ [], 3 ^ [])), less_than(3 ^ [], 3 ^ [])],extension(4,bind([[_19444, _19500, _19555], [4 ^ [], 3 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.2.2.1.1',plain,[less_than(4 ^ [], 3 ^ []), -(pair_in_list(update_slb(1 ^ [], 4 ^ []), 2 ^ [], 3 ^ [])), pair_in_list(1 ^ [], 2 ^ [], 3 ^ [])],extension(8,bind([[_28120, _27925, _27991, _28056], [4 ^ [], 1 ^ [], 2 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.2.2.1.1.1',plain,[pair_in_list(update_slb(1 ^ [], 4 ^ []), 2 ^ [], 3 ^ []), strictly_less_than(2 ^ [], 3 ^ [])],extension(3,bind([[_34150, _34155], [2 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.2.2.1.1.1.1',plain,[-(strictly_less_than(2 ^ [], 3 ^ []))],extension(2)).
% 0.83/1.41 cnf('1.2.2.1.1.2',plain,[-(pair_in_list(1 ^ [], 2 ^ [], 3 ^ []))],extension(1)).
% 0.83/1.41 cnf('1.2.2.1.2',plain,[-(less_than(3 ^ [], 3 ^ [])), -(less_than(3 ^ [], 3 ^ []))],extension(5,bind([[_19956, _19911], [3 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.2.2.1.2.1',plain,[less_than(3 ^ [], 3 ^ [])],reduction('1.2.2.1')).
% 0.83/1.41 cnf('1.2.2.2',plain,[-(less_than(2 ^ [], 3 ^ [])), -(less_than(3 ^ [], 2 ^ []))],extension(5,bind([[_19956, _19911], [3 ^ [], 2 ^ []]]))).
% 0.83/1.41 cnf('1.2.2.2.1',plain,[less_than(3 ^ [], 2 ^ []), -(less_than(3 ^ [], 2 ^ [])), less_than(2 ^ [], 2 ^ [])],extension(4,bind([[_19444, _19500, _19555], [3 ^ [], 2 ^ [], 2 ^ []]]))).
% 0.83/1.41 cnf('1.2.2.2.1.1',plain,[less_than(3 ^ [], 2 ^ []), strictly_less_than(2 ^ [], 3 ^ [])],extension(6,bind([[_20395, _20448], [2 ^ [], 3 ^ []]]))).
% 0.83/1.41 cnf('1.2.2.2.1.1.1',plain,[-(strictly_less_than(2 ^ [], 3 ^ []))],extension(2)).
% 0.83/1.41 cnf('1.2.2.2.1.2',plain,[-(less_than(2 ^ [], 2 ^ [])), -(less_than(2 ^ [], 2 ^ []))],extension(5,bind([[_19956, _19911], [2 ^ [], 2 ^ []]]))).
% 0.83/1.41 cnf('1.2.2.2.1.2.1',plain,[less_than(2 ^ [], 2 ^ [])],reduction('1.2.2.2.1')).
% 0.83/1.41 %-----------------------------------------------------
% 0.83/1.42
% 0.83/1.42 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------