%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GEO482+1 : TPTP v8.1.0. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n021.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 : Sat Jul 16 05:05:09 EDT 2022
% Result : Theorem 14.13s 14.86s
% Output : Proof 14.13s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : GEO482+1 : TPTP v8.1.0. Released v7.0.0.
% 0.06/0.12 % Command : leancop_casc.sh %s %d
% 0.13/0.33 % Computer : n021.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Sat Jun 18 15:15:01 EDT 2022
% 0.13/0.33 % CPUTime :
% 9.46/9.36
% 9.46/9.36 *** ECLiPSe fatal error: Out of swap space in heap allocation
% 10.93/10.71 calling an undefined procedure -(_3842075 = 0 ^ file('/export/starexec/sandbox/benchmark/theBenchmark.p', aINVERSEu_SWAP)) in module eclipse
% 10.93/10.71 abort
% 14.13/14.86 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.13/14.87 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.13/14.87
% 14.13/14.87 %-----------------------------------------------------
% 14.13/14.87 fof(aINVERSEu_SWAP, conjecture, ! [_2682047, _2682050, _2682053] : s(fun(_2682047, _2682047), i(s(fun(fun(_2682047, _2682047), fun(_2682047, _2682047)), inverse), s(fun(_2682047, _2682047), i(s(fun(prod(_2682047, _2682047), fun(_2682047, _2682047)), swap), s(prod(_2682047, _2682047), i(s(fun(_2682047, prod(_2682047, _2682047)), i(s(fun(_2682047, fun(_2682047, prod(_2682047, _2682047))), c_), s(_2682047, _2682050))), s(_2682047, _2682053))))))) = s(fun(_2682047, _2682047), i(s(fun(prod(_2682047, _2682047), fun(_2682047, _2682047)), swap), s(prod(_2682047, _2682047), i(s(fun(_2682047, prod(_2682047, _2682047)), i(s(fun(_2682047, fun(_2682047, prod(_2682047, _2682047))), c_), s(_2682047, _2682050))), s(_2682047, _2682053))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', aINVERSEu_SWAP)).
% 14.13/14.87 fof(aINVERSEu_UNIQUEu_o, axiom, ! [_2682950, _2682953, _2682956, _2682959] : (s(fun(_2682950, _2682950), i(s(fun(fun(_2682950, _2682953), fun(_2682950, _2682950)), i(s(fun(fun(_2682953, _2682950), fun(fun(_2682950, _2682953), fun(_2682950, _2682950))), o), s(fun(_2682953, _2682950), _2682956))), s(fun(_2682950, _2682953), _2682959))) = s(fun(_2682950, _2682950), i1) & s(fun(_2682953, _2682953), i(s(fun(fun(_2682953, _2682950), fun(_2682953, _2682953)), i(s(fun(fun(_2682950, _2682953), fun(fun(_2682953, _2682950), fun(_2682953, _2682953))), o), s(fun(_2682950, _2682953), _2682959))), s(fun(_2682953, _2682950), _2682956))) = s(fun(_2682953, _2682953), i1) => s(fun(_2682950, _2682953), i(s(fun(fun(_2682953, _2682950), fun(_2682950, _2682953)), inverse), s(fun(_2682953, _2682950), _2682956))) = s(fun(_2682950, _2682953), _2682959)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', aINVERSEu_UNIQUEu_o)).
% 14.13/14.87 fof(aSWAPu_IDEMPOTENT, axiom, ! [_2683953, _2683956, _2683959] : s(fun(_2683953, _2683953), i(s(fun(fun(_2683953, _2683953), fun(_2683953, _2683953)), i(s(fun(fun(_2683953, _2683953), fun(fun(_2683953, _2683953), fun(_2683953, _2683953))), o), s(fun(_2683953, _2683953), i(s(fun(prod(_2683953, _2683953), fun(_2683953, _2683953)), swap), s(prod(_2683953, _2683953), i(s(fun(_2683953, prod(_2683953, _2683953)), i(s(fun(_2683953, fun(_2683953, prod(_2683953, _2683953))), c_), s(_2683953, _2683956))), s(_2683953, _2683959))))))), s(fun(_2683953, _2683953), i(s(fun(prod(_2683953, _2683953), fun(_2683953, _2683953)), swap), s(prod(_2683953, _2683953), i(s(fun(_2683953, prod(_2683953, _2683953)), i(s(fun(_2683953, fun(_2683953, prod(_2683953, _2683953))), c_), s(_2683953, _2683956))), s(_2683953, _2683959))))))) = s(fun(_2683953, _2683953), i1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', aSWAPu_IDEMPOTENT)).
% 14.13/14.87
% 14.13/14.87 cnf(1, plain, [s(fun(7124 ^ [], 7124 ^ []), i(s(fun(fun(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), inverse), s(fun(7124 ^ [], 7124 ^ []), i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ []))))))) = s(fun(7124 ^ [], 7124 ^ []), i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ [])))))], clausify(aINVERSEu_SWAP)).
% 14.13/14.87 cnf(2, plain, [-(s(fun(_1494290, _1494291), i(s(fun(fun(_1494291, _1494290), fun(_1494290, _1494291)), inverse), s(fun(_1494291, _1494290), _1494292))) = s(fun(_1494290, _1494291), _1494293)), s(fun(_1494290, _1494290), i(s(fun(fun(_1494290, _1494291), fun(_1494290, _1494290)), i(s(fun(fun(_1494291, _1494290), fun(fun(_1494290, _1494291), fun(_1494290, _1494290))), o), s(fun(_1494291, _1494290), _1494292))), s(fun(_1494290, _1494291), _1494293))) = s(fun(_1494290, _1494290), i1), s(fun(_1494291, _1494291), i(s(fun(fun(_1494291, _1494290), fun(_1494291, _1494291)), i(s(fun(fun(_1494290, _1494291), fun(fun(_1494291, _1494290), fun(_1494291, _1494291))), o), s(fun(_1494290, _1494291), _1494293))), s(fun(_1494291, _1494290), _1494292))) = s(fun(_1494291, _1494291), i1)], clausify(aINVERSEu_UNIQUEu_o)).
% 14.13/14.87 cnf(3, plain, [-(s(fun(_1494709, _1494709), i(s(fun(fun(_1494709, _1494709), fun(_1494709, _1494709)), i(s(fun(fun(_1494709, _1494709), fun(fun(_1494709, _1494709), fun(_1494709, _1494709))), o), s(fun(_1494709, _1494709), i(s(fun(prod(_1494709, _1494709), fun(_1494709, _1494709)), swap), s(prod(_1494709, _1494709), i(s(fun(_1494709, prod(_1494709, _1494709)), i(s(fun(_1494709, fun(_1494709, prod(_1494709, _1494709))), c_), s(_1494709, _1494710))), s(_1494709, _1494711))))))), s(fun(_1494709, _1494709), i(s(fun(prod(_1494709, _1494709), fun(_1494709, _1494709)), swap), s(prod(_1494709, _1494709), i(s(fun(_1494709, prod(_1494709, _1494709)), i(s(fun(_1494709, fun(_1494709, prod(_1494709, _1494709))), c_), s(_1494709, _1494710))), s(_1494709, _1494711))))))) = s(fun(_1494709, _1494709), i1))], clausify(aSWAPu_IDEMPOTENT)).
% 14.13/14.87
% 14.13/14.87 cnf('1',plain,[s(fun(7124 ^ [], 7124 ^ []), i(s(fun(fun(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), inverse), s(fun(7124 ^ [], 7124 ^ []), i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ []))))))) = s(fun(7124 ^ [], 7124 ^ []), i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ [])))))],start(1)).
% 14.13/14.87 cnf('1.1',plain,[-(s(fun(7124 ^ [], 7124 ^ []), i(s(fun(fun(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), inverse), s(fun(7124 ^ [], 7124 ^ []), i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ []))))))) = s(fun(7124 ^ [], 7124 ^ []), i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ [])))))), s(fun(7124 ^ [], 7124 ^ []), i(s(fun(fun(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), i(s(fun(fun(7124 ^ [], 7124 ^ []), fun(fun(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ []))), o), s(fun(7124 ^ [], 7124 ^ []), i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ []))))))), s(fun(7124 ^ [], 7124 ^ []), i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ []))))))) = s(fun(7124 ^ [], 7124 ^ []), i1), s(fun(7124 ^ [], 7124 ^ []), i(s(fun(fun(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), i(s(fun(fun(7124 ^ [], 7124 ^ []), fun(fun(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ []))), o), s(fun(7124 ^ [], 7124 ^ []), i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ []))))))), s(fun(7124 ^ [], 7124 ^ []), i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ []))))))) = s(fun(7124 ^ [], 7124 ^ []), i1)],extension(2,bind([[_1494293, _1494290, _1494292, _1494291], [i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ [])))), 7124 ^ [], i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ [])))), 7124 ^ []]]))).
% 14.13/14.87 cnf('1.1.1',plain,[-(s(fun(7124 ^ [], 7124 ^ []), i(s(fun(fun(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), i(s(fun(fun(7124 ^ [], 7124 ^ []), fun(fun(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ []))), o), s(fun(7124 ^ [], 7124 ^ []), i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ []))))))), s(fun(7124 ^ [], 7124 ^ []), i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ []))))))) = s(fun(7124 ^ [], 7124 ^ []), i1))],extension(3,bind([[_1494710, _1494711, _1494709], [7125 ^ [], 7126 ^ [], 7124 ^ []]]))).
% 14.13/14.87 cnf('1.1.2',plain,[-(s(fun(7124 ^ [], 7124 ^ []), i(s(fun(fun(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), i(s(fun(fun(7124 ^ [], 7124 ^ []), fun(fun(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ []))), o), s(fun(7124 ^ [], 7124 ^ []), i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ []))))))), s(fun(7124 ^ [], 7124 ^ []), i(s(fun(prod(7124 ^ [], 7124 ^ []), fun(7124 ^ [], 7124 ^ [])), swap), s(prod(7124 ^ [], 7124 ^ []), i(s(fun(7124 ^ [], prod(7124 ^ [], 7124 ^ [])), i(s(fun(7124 ^ [], fun(7124 ^ [], prod(7124 ^ [], 7124 ^ []))), c_), s(7124 ^ [], 7125 ^ []))), s(7124 ^ [], 7126 ^ []))))))) = s(fun(7124 ^ [], 7124 ^ []), i1))],extension(3,bind([[_1494710, _1494711, _1494709], [7125 ^ [], 7126 ^ [], 7124 ^ []]]))).
% 14.13/14.87 %-----------------------------------------------------
% 14.13/14.88
% 14.13/14.88 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------