%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : COM146+1 : TPTP v8.1.0. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n017.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 : Fri Jul 15 01:28:15 EDT 2022
% Result : Theorem 29.18s 28.48s
% Output : Proof 29.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : COM146+1 : TPTP v8.1.0. Released v6.4.0.
% 0.12/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n017.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Thu Jun 16 18:07:11 EDT 2022
% 0.12/0.35 % CPUTime :
% 29.18/28.48 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.22/28.49 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.22/28.50
% 29.22/28.50 %-----------------------------------------------------
% 29.22/28.50 fof('EQ-noExp', axiom, (vnoExp = vnoExp => $ true) & ($ true => vnoExp = vnoExp), file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax', 'EQ-noExp')).
% 29.22/28.50 fof('T-Preservation-T-var', conjecture, ! [_171823, _171826, _171829, _171832] : (vreduce(vvar(_171823)) = vsomeExp(_171829) & vtcheck(_171826, vvar(_171823), _171832) => vtcheck(_171826, _171829, _171832)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'T-Preservation-T-var')).
% 29.22/28.50 fof(isSomeExp0, axiom, ! [_172190] : (_172190 = vnoExp => ~ visSomeExp(_172190)), file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax', isSomeExp0)).
% 29.22/28.50 fof(isSomeExp1, axiom, ! [_172321, _172324] : (_172324 = vsomeExp(_172321) => visSomeExp(_172324)), file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax', isSomeExp1)).
% 29.22/28.50 fof(reduce0, axiom, ! [_172466, _172469, _172472] : (_172469 = vvar(_172466) => _172472 = vreduce(_172469) => _172472 = vnoExp), file('/export/starexec/sandbox/benchmark/Axioms/COM001+0.ax', reduce0)).
% 29.22/28.50
% 29.22/28.50 cnf(1, plain, [-(55 ^ []), true___], clausify('EQ-noExp')).
% 29.22/28.50 cnf(2, plain, [-(55 ^ []), -(true___)], clausify('EQ-noExp')).
% 29.22/28.50 cnf(3, plain, [-(vreduce(vvar(106 ^ [])) = vsomeExp(108 ^ []))], clausify('T-Preservation-T-var')).
% 29.22/28.50 cnf(4, plain, [-(_50197 = _50197)], theory(equality)).
% 29.22/28.50 cnf(5, plain, [_50350 = _50395, -(_50395 = _50350)], theory(equality)).
% 29.22/28.50 cnf(6, plain, [-(_50629 = _50740), _50629 = _50685, _50685 = _50740], theory(equality)).
% 29.22/28.50 cnf(7, plain, [-(visSomeExp(_51778)), _51729 = _51778, visSomeExp(_51729)], theory(equality)).
% 29.22/28.50 cnf(8, plain, [55 ^ [], -(vnoExp = vnoExp)], clausify('EQ-noExp')).
% 29.22/28.50 cnf(9, plain, [_104984 = vnoExp, visSomeExp(_104984)], clausify(isSomeExp0)).
% 29.22/28.50 cnf(10, plain, [_105280 = vsomeExp(_105234), -(visSomeExp(_105280))], clausify(isSomeExp1)).
% 29.22/28.50 cnf(11, plain, [_106112 = vvar(_106052), _106171 = vreduce(_106112), -(_106171 = vnoExp)], clausify(reduce0)).
% 29.22/28.50
% 29.22/28.50 cnf('1',plain,[-(vreduce(vvar(106 ^ [])) = vsomeExp(108 ^ []))],start(3)).
% 29.22/28.50 cnf('1.1',plain,[vreduce(vvar(106 ^ [])) = vsomeExp(108 ^ []), -(vreduce(vvar(106 ^ [])) = vnoExp), vsomeExp(108 ^ []) = vnoExp],extension(6,bind([[_50629, _50685, _50740], [vreduce(vvar(106 ^ [])), vsomeExp(108 ^ []), vnoExp]]))).
% 29.22/28.50 cnf('1.1.1',plain,[vreduce(vvar(106 ^ [])) = vnoExp, -(visSomeExp(vnoExp)), visSomeExp(vreduce(vvar(106 ^ [])))],extension(7,bind([[_51778, _51729], [vnoExp, vreduce(vvar(106 ^ []))]]))).
% 29.22/28.50 cnf('1.1.1.1',plain,[visSomeExp(vnoExp), vnoExp = vnoExp],extension(9,bind([[_104984], [vnoExp]]))).
% 29.22/28.50 cnf('1.1.1.1.1',plain,[-(vnoExp = vnoExp), 55 ^ []],extension(8)).
% 29.22/28.50 cnf('1.1.1.1.1.1',plain,[-(55 ^ []), true___],extension(1)).
% 29.22/28.50 cnf('1.1.1.1.1.1.1',plain,[-(true___), -(55 ^ [])],extension(2)).
% 29.22/28.50 cnf('1.1.1.1.1.1.1.1',plain,[55 ^ []],reduction('1.1.1.1.1')).
% 29.22/28.50 cnf('1.1.1.2',plain,[-(visSomeExp(vreduce(vvar(106 ^ [])))), vreduce(vvar(106 ^ [])) = vsomeExp(108 ^ [])],extension(10,bind([[_105280, _105234], [vreduce(vvar(106 ^ [])), 108 ^ []]]))).
% 29.22/28.50 cnf('1.1.1.2.1',plain,[-(vreduce(vvar(106 ^ [])) = vsomeExp(108 ^ []))],extension(3)).
% 29.22/28.50 cnf('1.1.2',plain,[-(vsomeExp(108 ^ []) = vnoExp), vvar(106 ^ []) = vvar(106 ^ []), vsomeExp(108 ^ []) = vreduce(vvar(106 ^ []))],extension(11,bind([[_106052, _106171, _106112], [106 ^ [], vsomeExp(108 ^ []), vvar(106 ^ [])]]))).
% 29.22/28.50 cnf('1.1.2.1',plain,[-(vvar(106 ^ []) = vvar(106 ^ []))],extension(4,bind([[_50197], [vvar(106 ^ [])]]))).
% 29.22/28.50 cnf('1.1.2.2',plain,[-(vsomeExp(108 ^ []) = vreduce(vvar(106 ^ []))), vreduce(vvar(106 ^ [])) = vsomeExp(108 ^ [])],extension(5,bind([[_50350, _50395], [vreduce(vvar(106 ^ [])), vsomeExp(108 ^ [])]]))).
% 29.22/28.50 cnf('1.1.2.2.1',plain,[-(vreduce(vvar(106 ^ [])) = vsomeExp(108 ^ []))],extension(3)).
% 29.22/28.50 %-----------------------------------------------------
% 29.22/28.51
% 29.22/28.51 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------