%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KRS255+1 : TPTP v8.1.0. Bugfixed v5.4.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 : Sun Jul 17 03:14:05 EDT 2022
% Result : Theorem 0.40s 1.36s
% Output : Proof 0.40s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : KRS255+1 : TPTP v8.1.0. Bugfixed v5.4.0.
% 0.00/0.11 % Command : leancop_casc.sh %s %d
% 0.11/0.30 % Computer : n032.cluster.edu
% 0.11/0.30 % Model : x86_64 x86_64
% 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.30 % Memory : 8042.1875MB
% 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.30 % CPULimit : 300
% 0.11/0.30 % WCLimit : 600
% 0.11/0.30 % DateTime : Tue Jun 7 06:54:35 EDT 2022
% 0.11/0.30 % CPUTime :
% 0.40/1.36 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/1.37 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.40/1.37
% 0.40/1.37 %-----------------------------------------------------
% 0.40/1.37 fof(mighta_sap_thm, conjecture, mighta(sap, thm), file('/export/starexec/sandbox/benchmark/theBenchmark.p', mighta_sap_thm)).
% 0.40/1.37 fof(mighta, axiom, ! [_53489, _53492] : (? [_53500, _53503] : (status(_53500, _53503, _53489) & status(_53500, _53503, _53492)) <=> mighta(_53489, _53492)), file('/export/starexec/sandbox/benchmark/Axioms/KRS001+1.ax', mighta)).
% 0.40/1.37 fof(contradiction, axiom, ? [_53738] : ! [_53746] : ~ model(_53746, _53738), file('/export/starexec/sandbox/benchmark/Axioms/KRS001+1.ax', contradiction)).
% 0.40/1.37 fof(sap, axiom, ! [_53896, _53899] : (? [_53907] : model(_53907, _53896) => ? [_53925] : model(_53925, _53899) <=> status(_53896, _53899, sap)), file('/export/starexec/sandbox/benchmark/Axioms/KRS001+0.ax', sap)).
% 0.40/1.37 fof(thm, axiom, ! [_54146, _54149] : (! [_54157] : (model(_54157, _54146) => model(_54157, _54149)) <=> status(_54146, _54149, thm)), file('/export/starexec/sandbox/benchmark/Axioms/KRS001+0.ax', thm)).
% 0.40/1.37
% 0.40/1.37 cnf(1, plain, [mighta(sap, thm)], clausify(mighta_sap_thm)).
% 0.40/1.37 cnf(2, plain, [-(mighta(_25721, _25784)), status(_25857, _25913, _25721), status(_25857, _25913, _25784)], clausify(mighta)).
% 0.40/1.37 cnf(3, plain, [model(_38412, 56 ^ [])], clausify(contradiction)).
% 0.40/1.37 cnf(4, plain, [-(model(3 ^ [_13962, _13900], _13900)), -(status(_13900, _13962, sap))], clausify(sap)).
% 0.40/1.37 cnf(5, plain, [-(model(10 ^ [_15577, _15520], _15520)), -(status(_15520, _15577, thm))], clausify(thm)).
% 0.40/1.37
% 0.40/1.37 cnf('1',plain,[mighta(sap, thm)],start(1)).
% 0.40/1.37 cnf('1.1',plain,[-(mighta(sap, thm)), status(56 ^ [], _51229, sap), status(56 ^ [], _51229, thm)],extension(2,bind([[_25721, _25857, _25913, _25784], [sap, 56 ^ [], _51229, thm]]))).
% 0.40/1.37 cnf('1.1.1',plain,[-(status(56 ^ [], _51229, sap)), -(model(3 ^ [_51229, 56 ^ []], 56 ^ []))],extension(4,bind([[_13962, _13900], [_51229, 56 ^ []]]))).
% 0.40/1.37 cnf('1.1.1.1',plain,[model(3 ^ [_51229, 56 ^ []], 56 ^ [])],extension(3,bind([[_38412], [3 ^ [_51229, 56 ^ []]]]))).
% 0.40/1.37 cnf('1.1.2',plain,[-(status(56 ^ [], _51229, thm)), -(model(10 ^ [_51229, 56 ^ []], 56 ^ []))],extension(5,bind([[_15577, _15520], [_51229, 56 ^ []]]))).
% 0.40/1.37 cnf('1.1.2.1',plain,[model(10 ^ [_51229, 56 ^ []], 56 ^ [])],extension(3,bind([[_38412], [10 ^ [_51229, 56 ^ []]]]))).
% 0.40/1.37 %-----------------------------------------------------
% 0.40/1.38
% 0.40/1.38 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------