%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : KLE004+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n027.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 02:09:53 EDT 2022
% Result : Theorem 0.32s 1.41s
% Output : Proof 0.32s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KLE004+1 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : leancop_casc.sh %s %d
% 0.12/0.33 % Computer : n027.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 : Thu Jun 16 09:53:35 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.32/1.41 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.32/1.41 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.32/1.42
% 0.32/1.42 %-----------------------------------------------------
% 0.32/1.42 fof(goals, conjecture, c(zero) = one, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals)).
% 0.32/1.42 fof(additive_commutativity, axiom, ! [_26986, _26989] : addition(_26986, _26989) = addition(_26989, _26986), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax', additive_commutativity)).
% 0.32/1.42 fof(additive_identity, axiom, ! [_27133] : addition(_27133, zero) = _27133, file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax', additive_identity)).
% 0.32/1.42 fof(multiplicative_right_identity, axiom, ! [_27254] : multiplication(_27254, one) = _27254, file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax', multiplicative_right_identity)).
% 0.32/1.42 fof(multiplicative_left_identity, axiom, ! [_27373] : multiplication(one, _27373) = _27373, file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax', multiplicative_left_identity)).
% 0.32/1.42 fof(test_1, axiom, ! [_27499] : (test(_27499) <=> ? [_27514] : complement(_27514, _27499)), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+1.ax', test_1)).
% 0.32/1.42 fof(test_2, axiom, ! [_27660, _27663] : (complement(_27663, _27660) <=> multiplication(_27660, _27663) = zero & multiplication(_27663, _27660) = zero & addition(_27660, _27663) = one), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+1.ax', test_2)).
% 0.32/1.42 fof(test_3, axiom, ! [_27900, _27903] : (test(_27900) => (c(_27900) = _27903 <=> complement(_27900, _27903))), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+1.ax', test_3)).
% 0.32/1.42
% 0.32/1.42 cnf(1, plain, [c(zero) = one], clausify(goals)).
% 0.32/1.42 cnf(2, plain, [-(addition(_12469, _12514) = addition(_12514, _12469))], clausify(additive_commutativity)).
% 0.32/1.42 cnf(3, plain, [-(addition(_13246, zero) = _13246)], clausify(additive_identity)).
% 0.32/1.42 cnf(4, plain, [-(multiplication(_14141, one) = _14141)], clausify(multiplicative_right_identity)).
% 0.32/1.42 cnf(5, plain, [-(multiplication(one, _14355) = _14355)], clausify(multiplicative_left_identity)).
% 0.32/1.42 cnf(6, plain, [-(test(_16531)), complement(_16614, _16531)], clausify(test_1)).
% 0.32/1.42 cnf(7, plain, [-(complement(_16880, _16814)), multiplication(_16814, _16880) = zero, multiplication(_16880, _16814) = zero, addition(_16814, _16880) = one], clausify(test_2)).
% 0.32/1.42 cnf(8, plain, [test(_17425), -(c(_17425) = _17477), complement(_17425, _17477)], clausify(test_3)).
% 0.32/1.42 cnf(9, plain, [-(_8738 = _8849), _8738 = _8794, _8794 = _8849], theory(equality)).
% 0.32/1.42
% 0.32/1.42 cnf('1',plain,[c(zero) = one],start(1)).
% 0.32/1.42 cnf('1.1',plain,[-(c(zero) = one), test(zero), complement(zero, one)],extension(8,bind([[_17425, _17477], [zero, one]]))).
% 0.32/1.42 cnf('1.1.1',plain,[-(test(zero)), complement(one, zero)],extension(6,bind([[_16614, _16531], [one, zero]]))).
% 0.32/1.42 cnf('1.1.1.1',plain,[-(complement(one, zero)), multiplication(zero, one) = zero, multiplication(one, zero) = zero, addition(zero, one) = one],extension(7,bind([[_16814, _16880], [zero, one]]))).
% 0.32/1.42 cnf('1.1.1.1.1',plain,[-(multiplication(zero, one) = zero)],extension(4,bind([[_14141], [zero]]))).
% 0.32/1.42 cnf('1.1.1.1.2',plain,[-(multiplication(one, zero) = zero)],extension(5,bind([[_14355], [zero]]))).
% 0.32/1.42 cnf('1.1.1.1.3',plain,[-(addition(zero, one) = one), addition(zero, one) = addition(one, zero), addition(one, zero) = one],extension(9,bind([[_8738, _8794, _8849], [addition(zero, one), addition(one, zero), one]]))).
% 0.32/1.42 cnf('1.1.1.1.3.1',plain,[-(addition(zero, one) = addition(one, zero))],extension(2,bind([[_12514, _12469], [one, zero]]))).
% 0.32/1.42 cnf('1.1.1.1.3.2',plain,[-(addition(one, zero) = one)],extension(3,bind([[_13246], [one]]))).
% 0.32/1.42 cnf('1.1.2',plain,[-(complement(zero, one)), multiplication(one, zero) = zero, multiplication(zero, one) = zero, addition(one, zero) = one],extension(7,bind([[_16814, _16880], [one, zero]]))).
% 0.32/1.42 cnf('1.1.2.1',plain,[-(multiplication(one, zero) = zero)],extension(5,bind([[_14355], [zero]]))).
% 0.32/1.42 cnf('1.1.2.2',plain,[-(multiplication(zero, one) = zero)],extension(4,bind([[_14141], [zero]]))).
% 0.32/1.42 cnf('1.1.2.3',plain,[-(addition(one, zero) = one)],extension(3,bind([[_13246], [one]]))).
% 0.32/1.42 %-----------------------------------------------------
% 0.32/1.42
% 0.32/1.43 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------