%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SET077+1 : TPTP v8.1.0. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n003.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 02:51:03 EDT 2022
% Result : Theorem 0.36s 1.40s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SET077+1 : TPTP v8.1.0. Bugfixed v5.4.0.
% 0.10/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n003.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Mon Jul 11 00:27:45 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.36/1.40 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.41 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.41
% 0.36/1.41 %-----------------------------------------------------
% 0.36/1.41 fof(singletons_are_sets, conjecture, ! [_74844] : member(singleton(_74844), universal_class), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', singletons_are_sets)).
% 0.36/1.41 fof(unordered_pair, axiom, ! [_75033, _75036] : member(unordered_pair(_75033, _75036), universal_class), file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax', unordered_pair)).
% 0.36/1.41 fof(singleton_set_defn, axiom, ! [_75167] : singleton(_75167) = unordered_pair(_75167, _75167), file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax', singleton_set_defn)).
% 0.36/1.41
% 0.36/1.41 cnf(1, plain, [member(singleton(8 ^ []), universal_class)], clausify(singletons_are_sets)).
% 0.36/1.41 cnf(2, plain, [-(_22539 = _22539)], theory(equality)).
% 0.36/1.41 cnf(3, plain, [_22692 = _22737, -(_22737 = _22692)], theory(equality)).
% 0.36/1.41 cnf(4, plain, [-(member(_24796, _24927)), member(_24729, _24862), _24729 = _24796, _24862 = _24927], theory(equality)).
% 0.36/1.41 cnf(5, plain, [-(member(unordered_pair(_37969, _38011), universal_class))], clausify(unordered_pair)).
% 0.36/1.41 cnf(6, plain, [-(singleton(_38236) = unordered_pair(_38236, _38236))], clausify(singleton_set_defn)).
% 0.36/1.41
% 0.36/1.41 cnf('1',plain,[member(singleton(8 ^ []), universal_class)],start(1)).
% 0.36/1.41 cnf('1.1',plain,[-(member(singleton(8 ^ []), universal_class)), member(unordered_pair(8 ^ [], 8 ^ []), universal_class), unordered_pair(8 ^ [], 8 ^ []) = singleton(8 ^ []), universal_class = universal_class],extension(4,bind([[_24729, _24796, _24862, _24927], [unordered_pair(8 ^ [], 8 ^ []), singleton(8 ^ []), universal_class, universal_class]]))).
% 0.36/1.41 cnf('1.1.1',plain,[-(member(unordered_pair(8 ^ [], 8 ^ []), universal_class)), member(unordered_pair(8 ^ [], 8 ^ []), universal_class), unordered_pair(8 ^ [], 8 ^ []) = unordered_pair(8 ^ [], 8 ^ []), universal_class = universal_class],extension(4,bind([[_24729, _24796, _24862, _24927], [unordered_pair(8 ^ [], 8 ^ []), unordered_pair(8 ^ [], 8 ^ []), universal_class, universal_class]]))).
% 0.36/1.41 cnf('1.1.1.1',plain,[-(member(unordered_pair(8 ^ [], 8 ^ []), universal_class))],extension(5,bind([[_37969, _38011], [8 ^ [], 8 ^ []]]))).
% 0.36/1.41 cnf('1.1.1.2',plain,[-(unordered_pair(8 ^ [], 8 ^ []) = unordered_pair(8 ^ [], 8 ^ []))],extension(2,bind([[_22539], [unordered_pair(8 ^ [], 8 ^ [])]]))).
% 0.36/1.41 cnf('1.1.1.3',plain,[-(universal_class = universal_class)],extension(2,bind([[_22539], [universal_class]]))).
% 0.36/1.41 cnf('1.1.2',plain,[-(unordered_pair(8 ^ [], 8 ^ []) = singleton(8 ^ [])), singleton(8 ^ []) = unordered_pair(8 ^ [], 8 ^ [])],extension(3,bind([[_22692, _22737], [singleton(8 ^ []), unordered_pair(8 ^ [], 8 ^ [])]]))).
% 0.36/1.41 cnf('1.1.2.1',plain,[-(singleton(8 ^ []) = unordered_pair(8 ^ [], 8 ^ []))],extension(6,bind([[_38236], [8 ^ []]]))).
% 0.36/1.41 cnf('1.1.3',plain,[-(universal_class = universal_class)],extension(2,bind([[_22539], [universal_class]]))).
% 0.36/1.41 %-----------------------------------------------------
% 0.36/1.42
% 0.36/1.42 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------