%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU257+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n032.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 : Tue Jul 19 12:01:29 EDT 2022
% Result : Theorem 0.25s 1.33s
% Output : Proof 0.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.08 % Problem : SEU257+1 : TPTP v8.1.0. Released v3.3.0.
% 0.00/0.09 % Command : leancop_casc.sh %s %d
% 0.07/0.27 % Computer : n032.cluster.edu
% 0.07/0.27 % Model : x86_64 x86_64
% 0.07/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.27 % Memory : 8042.1875MB
% 0.07/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.27 % CPULimit : 300
% 0.07/0.27 % WCLimit : 600
% 0.07/0.27 % DateTime : Mon Jun 20 04:35:03 EDT 2022
% 0.07/0.27 % CPUTime :
% 0.25/1.33 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.25/1.34 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.25/1.34
% 0.25/1.34 %-----------------------------------------------------
% 0.25/1.34 fof(t32_wellord1, conjecture, ! [_27963, _27966] : (relation(_27966) => well_ordering(_27966) => well_ordering(relation_restriction(_27966, _27963))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t32_wellord1)).
% 0.25/1.34 fof(d4_wellord1, axiom, ! [_28155] : (relation(_28155) => (well_ordering(_28155) <=> reflexive(_28155) & transitive(_28155) & antisymmetric(_28155) & connected(_28155) & well_founded_relation(_28155))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d4_wellord1)).
% 0.25/1.34 fof(dt_k2_wellord1, axiom, ! [_28442, _28445] : (relation(_28442) => relation(relation_restriction(_28442, _28445))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', dt_k2_wellord1)).
% 0.25/1.34 fof(t22_wellord1, axiom, ! [_28591, _28594] : (relation(_28594) => reflexive(_28594) => reflexive(relation_restriction(_28594, _28591))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t22_wellord1)).
% 0.25/1.34 fof(t23_wellord1, axiom, ! [_28760, _28763] : (relation(_28763) => connected(_28763) => connected(relation_restriction(_28763, _28760))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t23_wellord1)).
% 0.25/1.34 fof(t24_wellord1, axiom, ! [_28929, _28932] : (relation(_28932) => transitive(_28932) => transitive(relation_restriction(_28932, _28929))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t24_wellord1)).
% 0.25/1.34 fof(t25_wellord1, axiom, ! [_29098, _29101] : (relation(_29101) => antisymmetric(_29101) => antisymmetric(relation_restriction(_29101, _29098))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t25_wellord1)).
% 0.25/1.34 fof(t31_wellord1, axiom, ! [_29267, _29270] : (relation(_29270) => well_founded_relation(_29270) => well_founded_relation(relation_restriction(_29270, _29267))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t31_wellord1)).
% 0.25/1.34
% 0.25/1.34 cnf(1, plain, [-(relation(2 ^ []))], clausify(t32_wellord1)).
% 0.25/1.34 cnf(2, plain, [-(well_ordering(2 ^ []))], clausify(t32_wellord1)).
% 0.25/1.34 cnf(3, plain, [well_ordering(relation_restriction(2 ^ [], 1 ^ []))], clausify(t32_wellord1)).
% 0.25/1.34 cnf(4, plain, [relation(_12825), well_ordering(_12825), -(reflexive(_12825))], clausify(d4_wellord1)).
% 0.25/1.34 cnf(5, plain, [relation(_12825), well_ordering(_12825), -(transitive(_12825))], clausify(d4_wellord1)).
% 0.25/1.34 cnf(6, plain, [relation(_12825), well_ordering(_12825), -(antisymmetric(_12825))], clausify(d4_wellord1)).
% 0.25/1.34 cnf(7, plain, [relation(_12825), well_ordering(_12825), -(connected(_12825))], clausify(d4_wellord1)).
% 0.25/1.34 cnf(8, plain, [relation(_12825), well_ordering(_12825), -(well_founded_relation(_12825))], clausify(d4_wellord1)).
% 0.25/1.34 cnf(9, plain, [relation(_12825), -(well_ordering(_12825)), reflexive(_12825), transitive(_12825), antisymmetric(_12825), connected(_12825), well_founded_relation(_12825)], clausify(d4_wellord1)).
% 0.25/1.34 cnf(10, plain, [relation(_13736), -(relation(relation_restriction(_13736, _13782)))], clausify(dt_k2_wellord1)).
% 0.25/1.34 cnf(11, plain, [relation(_14627), reflexive(_14627), -(reflexive(relation_restriction(_14627, _14576)))], clausify(t22_wellord1)).
% 0.25/1.34 cnf(12, plain, [relation(_14997), connected(_14997), -(connected(relation_restriction(_14997, _14946)))], clausify(t23_wellord1)).
% 0.25/1.34 cnf(13, plain, [relation(_15367), transitive(_15367), -(transitive(relation_restriction(_15367, _15316)))], clausify(t24_wellord1)).
% 0.25/1.34 cnf(14, plain, [relation(_15737), antisymmetric(_15737), -(antisymmetric(relation_restriction(_15737, _15686)))], clausify(t25_wellord1)).
% 0.25/1.34 cnf(15, plain, [relation(_16097), well_founded_relation(_16097), -(well_founded_relation(relation_restriction(_16097, _16046)))], clausify(t31_wellord1)).
% 0.25/1.34
% 0.25/1.34 cnf('1',plain,[well_ordering(relation_restriction(2 ^ [], 1 ^ []))],start(3)).
% 0.25/1.34 cnf('1.1',plain,[-(well_ordering(relation_restriction(2 ^ [], 1 ^ []))), relation(relation_restriction(2 ^ [], 1 ^ [])), reflexive(relation_restriction(2 ^ [], 1 ^ [])), transitive(relation_restriction(2 ^ [], 1 ^ [])), antisymmetric(relation_restriction(2 ^ [], 1 ^ [])), connected(relation_restriction(2 ^ [], 1 ^ [])), well_founded_relation(relation_restriction(2 ^ [], 1 ^ []))],extension(9,bind([[_12825], [relation_restriction(2 ^ [], 1 ^ [])]]))).
% 0.25/1.34 cnf('1.1.1',plain,[-(relation(relation_restriction(2 ^ [], 1 ^ []))), relation(2 ^ [])],extension(10,bind([[_13782, _13736], [1 ^ [], 2 ^ []]]))).
% 0.25/1.34 cnf('1.1.1.1',plain,[-(relation(2 ^ []))],extension(1)).
% 0.25/1.34 cnf('1.1.2',plain,[-(reflexive(relation_restriction(2 ^ [], 1 ^ []))), relation(2 ^ []), reflexive(2 ^ [])],extension(11,bind([[_14576, _14627], [1 ^ [], 2 ^ []]]))).
% 0.25/1.34 cnf('1.1.2.1',plain,[-(relation(2 ^ []))],extension(1)).
% 0.25/1.34 cnf('1.1.2.2',plain,[-(reflexive(2 ^ [])), relation(2 ^ []), well_ordering(2 ^ [])],extension(4,bind([[_12825], [2 ^ []]]))).
% 0.25/1.34 cnf('1.1.2.2.1',plain,[-(relation(2 ^ []))],extension(1)).
% 0.25/1.34 cnf('1.1.2.2.2',plain,[-(well_ordering(2 ^ []))],extension(2)).
% 0.25/1.34 cnf('1.1.3',plain,[-(transitive(relation_restriction(2 ^ [], 1 ^ []))), relation(2 ^ []), transitive(2 ^ [])],extension(13,bind([[_15316, _15367], [1 ^ [], 2 ^ []]]))).
% 0.25/1.34 cnf('1.1.3.1',plain,[-(relation(2 ^ []))],extension(1)).
% 0.25/1.34 cnf('1.1.3.2',plain,[-(transitive(2 ^ [])), relation(2 ^ []), well_ordering(2 ^ [])],extension(5,bind([[_12825], [2 ^ []]]))).
% 0.25/1.34 cnf('1.1.3.2.1',plain,[-(relation(2 ^ []))],extension(1)).
% 0.25/1.34 cnf('1.1.3.2.2',plain,[-(well_ordering(2 ^ []))],extension(2)).
% 0.25/1.34 cnf('1.1.4',plain,[-(antisymmetric(relation_restriction(2 ^ [], 1 ^ []))), relation(2 ^ []), antisymmetric(2 ^ [])],extension(14,bind([[_15686, _15737], [1 ^ [], 2 ^ []]]))).
% 0.25/1.34 cnf('1.1.4.1',plain,[-(relation(2 ^ []))],extension(1)).
% 0.25/1.34 cnf('1.1.4.2',plain,[-(antisymmetric(2 ^ [])), relation(2 ^ []), well_ordering(2 ^ [])],extension(6,bind([[_12825], [2 ^ []]]))).
% 0.25/1.34 cnf('1.1.4.2.1',plain,[-(relation(2 ^ []))],extension(1)).
% 0.25/1.34 cnf('1.1.4.2.2',plain,[-(well_ordering(2 ^ []))],extension(2)).
% 0.25/1.34 cnf('1.1.5',plain,[-(connected(relation_restriction(2 ^ [], 1 ^ []))), relation(2 ^ []), connected(2 ^ [])],extension(12,bind([[_14946, _14997], [1 ^ [], 2 ^ []]]))).
% 0.25/1.34 cnf('1.1.5.1',plain,[-(relation(2 ^ []))],extension(1)).
% 0.25/1.34 cnf('1.1.5.2',plain,[-(connected(2 ^ [])), relation(2 ^ []), well_ordering(2 ^ [])],extension(7,bind([[_12825], [2 ^ []]]))).
% 0.25/1.34 cnf('1.1.5.2.1',plain,[-(relation(2 ^ []))],extension(1)).
% 0.25/1.34 cnf('1.1.5.2.2',plain,[-(well_ordering(2 ^ []))],extension(2)).
% 0.25/1.34 cnf('1.1.6',plain,[-(well_founded_relation(relation_restriction(2 ^ [], 1 ^ []))), relation(2 ^ []), well_founded_relation(2 ^ [])],extension(15,bind([[_16046, _16097], [1 ^ [], 2 ^ []]]))).
% 0.25/1.34 cnf('1.1.6.1',plain,[-(relation(2 ^ []))],extension(1)).
% 0.25/1.34 cnf('1.1.6.2',plain,[-(well_founded_relation(2 ^ [])), relation(2 ^ []), well_ordering(2 ^ [])],extension(8,bind([[_12825], [2 ^ []]]))).
% 0.25/1.34 cnf('1.1.6.2.1',plain,[-(relation(2 ^ []))],extension(1)).
% 0.25/1.34 cnf('1.1.6.2.2',plain,[-(well_ordering(2 ^ []))],extension(2)).
% 0.25/1.34 %-----------------------------------------------------
% 0.25/1.35
% 0.25/1.35 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------