%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEU268+1 : TPTP v8.1.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n009.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:34 EDT 2022
% Result : Theorem 0.86s 1.41s
% Output : Proof 0.86s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU268+1 : TPTP v8.1.0. Released v3.3.0.
% 0.03/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n009.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Sun Jun 19 04:34:07 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.86/1.41 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.86/1.42 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.86/1.42
% 0.86/1.42 %-----------------------------------------------------
% 0.86/1.42 fof(t2_wellord2, conjecture, ! [_67524] : reflexive(inclusion_relation(_67524)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', t2_wellord2)).
% 0.86/1.42 fof(d1_relat_2, axiom, ! [_67713] : (relation(_67713) => ! [_67728] : (is_reflexive_in(_67713, _67728) <=> ! [_67746] : (in(_67746, _67728) => in(ordered_pair(_67746, _67746), _67713)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_relat_2)).
% 0.86/1.42 fof(d1_wellord2, axiom, ! [_67990, _67993] : (relation(_67993) => (_67993 = inclusion_relation(_67990) <=> relation_field(_67993) = _67990 & ! [_68028, _68031] : (in(_68028, _67990) & in(_68031, _67990) => (in(ordered_pair(_68028, _68031), _67993) <=> subset(_68028, _68031))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d1_wellord2)).
% 0.86/1.42 fof(d9_relat_2, axiom, ! [_68352] : (relation(_68352) => (reflexive(_68352) <=> is_reflexive_in(_68352, relation_field(_68352)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', d9_relat_2)).
% 0.86/1.42 fof(dt_k1_wellord2, axiom, ! [_68510] : relation(inclusion_relation(_68510)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', dt_k1_wellord2)).
% 0.86/1.42 fof(reflexivity_r1_tarski, axiom, ! [_68660, _68663] : subset(_68660, _68660), file('/export/starexec/sandbox/benchmark/theBenchmark.p', reflexivity_r1_tarski)).
% 0.86/1.42
% 0.86/1.42 cnf(1, plain, [reflexive(inclusion_relation(14 ^ []))], clausify(t2_wellord2)).
% 0.86/1.42 cnf(2, plain, [_24971 = _25020, -(inclusion_relation(_24971) = inclusion_relation(_25020))], theory(equality)).
% 0.86/1.42 cnf(3, plain, [-(_18421 = _18421)], theory(equality)).
% 0.86/1.42 cnf(4, plain, [-(in(_21336, _21467)), in(_21269, _21402), _21269 = _21336, _21402 = _21467], theory(equality)).
% 0.86/1.42 cnf(5, plain, [-(subset(_24219, _24350)), subset(_24152, _24285), _24152 = _24219, _24285 = _24350], theory(equality)).
% 0.86/1.42 cnf(6, plain, [relation(_31427), -(is_reflexive_in(_31427, _31529)), -(in(1 ^ [_31529, _31427], _31529))], clausify(d1_relat_2)).
% 0.86/1.42 cnf(7, plain, [relation(_31427), -(is_reflexive_in(_31427, _31529)), in(ordered_pair(1 ^ [_31529, _31427], 1 ^ [_31529, _31427]), _31427)], clausify(d1_relat_2)).
% 0.86/1.42 cnf(8, plain, [relation(_32083), _32083 = inclusion_relation(_31992), -(relation_field(_32083) = _31992)], clausify(d1_wellord2)).
% 0.86/1.42 cnf(9, plain, [relation(_32083), _32083 = inclusion_relation(_31992), in(_32429, _31992), in(_32361, _31992), -(in(ordered_pair(_32361, _32429), _32083)), subset(_32361, _32429)], clausify(d1_wellord2)).
% 0.86/1.42 cnf(10, plain, [relation(_33660), -(reflexive(_33660)), is_reflexive_in(_33660, relation_field(_33660))], clausify(d9_relat_2)).
% 0.86/1.42 cnf(11, plain, [-(relation(inclusion_relation(_34234)))], clausify(dt_k1_wellord2)).
% 0.86/1.42 cnf(12, plain, [-(subset(_39970, _39970))], clausify(reflexivity_r1_tarski)).
% 0.86/1.42
% 0.86/1.42 cnf('1',plain,[reflexive(inclusion_relation(14 ^ []))],start(1)).
% 0.86/1.42 cnf('1.1',plain,[-(reflexive(inclusion_relation(14 ^ []))), relation(inclusion_relation(14 ^ [])), is_reflexive_in(inclusion_relation(14 ^ []), relation_field(inclusion_relation(14 ^ [])))],extension(10,bind([[_33660], [inclusion_relation(14 ^ [])]]))).
% 0.86/1.42 cnf('1.1.1',plain,[-(relation(inclusion_relation(14 ^ [])))],extension(11,bind([[_34234], [14 ^ []]]))).
% 0.86/1.42 cnf('1.1.2',plain,[-(is_reflexive_in(inclusion_relation(14 ^ []), relation_field(inclusion_relation(14 ^ [])))), relation(inclusion_relation(14 ^ [])), in(ordered_pair(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]), inclusion_relation(14 ^ []))],extension(7,bind([[_31529, _31427], [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]]))).
% 0.86/1.42 cnf('1.1.2.1',plain,[-(relation(inclusion_relation(14 ^ [])))],extension(11,bind([[_34234], [14 ^ []]]))).
% 0.86/1.42 cnf('1.1.2.2',plain,[-(in(ordered_pair(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]), inclusion_relation(14 ^ []))), relation(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ []) = inclusion_relation(14 ^ []), in(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 14 ^ []), in(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 14 ^ []), subset(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])])],extension(9,bind([[_32083, _31992, _32361, _32429], [inclusion_relation(14 ^ []), 14 ^ [], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]]]))).
% 0.86/1.42 cnf('1.1.2.2.1',plain,[-(relation(inclusion_relation(14 ^ [])))],extension(11,bind([[_34234], [14 ^ []]]))).
% 0.86/1.42 cnf('1.1.2.2.2',plain,[-(inclusion_relation(14 ^ []) = inclusion_relation(14 ^ [])), 14 ^ [] = 14 ^ []],extension(2,bind([[_24971, _25020], [14 ^ [], 14 ^ []]]))).
% 0.86/1.42 cnf('1.1.2.2.2.1',plain,[-(14 ^ [] = 14 ^ [])],extension(3,bind([[_18421], [14 ^ []]]))).
% 0.86/1.42 cnf('1.1.2.2.3',plain,[-(in(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 14 ^ [])), in(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], relation_field(inclusion_relation(14 ^ []))), 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])] = 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], relation_field(inclusion_relation(14 ^ [])) = 14 ^ []],extension(4,bind([[_21269, _21336, _21402, _21467], [1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], relation_field(inclusion_relation(14 ^ [])), 14 ^ []]]))).
% 0.86/1.42 cnf('1.1.2.2.3.1',plain,[-(in(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], relation_field(inclusion_relation(14 ^ [])))), relation(inclusion_relation(14 ^ [])), -(is_reflexive_in(inclusion_relation(14 ^ []), relation_field(inclusion_relation(14 ^ []))))],extension(6,bind([[_31427, _31529], [inclusion_relation(14 ^ []), relation_field(inclusion_relation(14 ^ []))]]))).
% 0.86/1.42 cnf('1.1.2.2.3.1.1',plain,[-(relation(inclusion_relation(14 ^ [])))],extension(11,bind([[_34234], [14 ^ []]]))).
% 0.86/1.42 cnf('1.1.2.2.3.1.2',plain,[is_reflexive_in(inclusion_relation(14 ^ []), relation_field(inclusion_relation(14 ^ [])))],reduction('1.1')).
% 0.86/1.42 cnf('1.1.2.2.3.2',plain,[-(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])] = 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])])],extension(3,bind([[_18421], [1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]]]))).
% 0.86/1.42 cnf('1.1.2.2.3.3',plain,[-(relation_field(inclusion_relation(14 ^ [])) = 14 ^ []), relation(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ []) = inclusion_relation(14 ^ [])],extension(8,bind([[_32083, _31992], [inclusion_relation(14 ^ []), 14 ^ []]]))).
% 0.86/1.42 cnf('1.1.2.2.3.3.1',plain,[-(relation(inclusion_relation(14 ^ [])))],extension(11,bind([[_34234], [14 ^ []]]))).
% 0.86/1.42 cnf('1.1.2.2.3.3.2',plain,[-(inclusion_relation(14 ^ []) = inclusion_relation(14 ^ []))],extension(3,bind([[_18421], [inclusion_relation(14 ^ [])]]))).
% 0.86/1.42 cnf('1.1.2.2.4',plain,[-(in(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 14 ^ []))],lemmata('1.1.2.2')).
% 0.86/1.42 cnf('1.1.2.2.5',plain,[-(subset(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])])), subset(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]), 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])] = 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])] = 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]],extension(5,bind([[_24152, _24219, _24285, _24350], [1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]]]))).
% 0.86/1.42 cnf('1.1.2.2.5.1',plain,[-(subset(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])])), subset(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]), 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])] = 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])] = 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]],extension(5,bind([[_24152, _24219, _24285, _24350], [1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]]]))).
% 0.86/1.42 cnf('1.1.2.2.5.1.1',plain,[-(subset(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])], 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]))],extension(12,bind([[_39970], [1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]]]))).
% 0.86/1.42 cnf('1.1.2.2.5.1.2',plain,[-(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])] = 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])])],extension(3,bind([[_18421], [1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]]]))).
% 0.86/1.42 cnf('1.1.2.2.5.1.3',plain,[-(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])] = 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])])],extension(3,bind([[_18421], [1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]]]))).
% 0.86/1.42 cnf('1.1.2.2.5.2',plain,[-(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])] = 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])])],extension(3,bind([[_18421], [1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]]]))).
% 0.86/1.42 cnf('1.1.2.2.5.3',plain,[-(1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])] = 1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])])],extension(3,bind([[_18421], [1 ^ [relation_field(inclusion_relation(14 ^ [])), inclusion_relation(14 ^ [])]]]))).
% 0.86/1.42 %-----------------------------------------------------
% 0.86/1.43
% 0.86/1.43 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------