%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GEO271+1 : TPTP v8.1.0. Released v4.1.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 : Sat Jul 16 05:04:20 EDT 2022
% Result : Theorem 29.31s 29.32s
% Output : Proof 29.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GEO271+1 : TPTP v8.1.0. Released v4.1.0.
% 0.04/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 : Fri Jun 17 21:39:42 EDT 2022
% 0.12/0.34 % CPUTime :
% 29.31/29.32 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.31/29.32 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.31/29.33
% 29.31/29.33 %-----------------------------------------------------
% 29.31/29.33 fof('qu(cond(axiom(184), 0), imp(cond(axiom(184), 0)))', axiom, ! [_434869, _434872, _434875, _434878, _434881, _434884] : (ron(_434881, _434878) & _434881 = _434884 & rpoint(_434884) & rcenter(_434875, _434878) & _434869 = _434872 & rpoint(_434872) => (vf(_434875, _434869) = vf(_434875, _434881) <=> ron(_434869, _434878))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'qu(cond(axiom(184), 0), imp(cond(axiom(184), 0)))')).
% 29.31/29.33 fof('qu(theu(the(211), 1), imp(the(211)))', conjecture, ! [_435270] : (ron(vd1057, _435270) & rcenter(vd1055, _435270) & rcircle(_435270) => _435270 = vd1061), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'qu(theu(the(211), 1), imp(the(211)))')).
% 29.31/29.33 fof('and(pred(comma_conjunct2(the(211)), 0), and(pred(comma_conjunct1(the(211)), 0), pred(the(211), 0)))', axiom, ron(vd1057, vd1061) & rcenter(vd1055, vd1061) & rcircle(vd1061), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'and(pred(comma_conjunct2(the(211)), 0), and(pred(comma_conjunct1(the(211)), 0), pred(the(211), 0)))')).
% 29.31/29.33 fof('and(pred(conjunct2(210), 4), and(holds(conjunct2(210), 1059, 0), and(pred(conjunct2(210), 1), and(pred(conjunct1(210), 2), pred(conjunct1(210), 1)))))', axiom, vd1057 = vd1058 & (! vd1055) = vd1057 & rpoint(vd1058) & vd1055 = vd1056 & rpoint(vd1056), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'and(pred(conjunct2(210), 4), and(holds(conjunct2(210), 1059, 0), and(pred(conjunct2(210), 1), and(pred(conjunct1(210), 2), pred(conjunct1(210), 1)))))')).
% 29.31/29.33 fof('qu(cond(axiom(182), 0), imp(cond(axiom(182), 0)))', axiom, ! [_435687, _435690, _435693, _435696, _435699] : (vf(_435693, _435687) = vf(_435693, _435690) & ron(_435690, _435699) & ron(_435687, _435696) & rcenter(_435693, _435699) & rcenter(_435693, _435696) & ? [_435767] : (_435690 = _435767 & rpoint(_435767)) & ? [_435788] : (_435687 = _435788 & rpoint(_435788)) => _435696 = _435699), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'qu(cond(axiom(182), 0), imp(cond(axiom(182), 0)))')).
% 29.31/29.33
% 29.31/29.33 cnf(1, plain, [-(17 ^ [_194858, _194757, _194655, _194552, _194448, _194343]), -(vf(_194552, _194343) = vf(_194552, _194757)), ron(_194343, _194655)], clausify('qu(cond(axiom(184), 0), imp(cond(axiom(184), 0)))')).
% 29.31/29.33 cnf(2, plain, [-(ron(vd1057, 110 ^ []))], clausify('qu(theu(the(211), 1), imp(the(211)))')).
% 29.31/29.33 cnf(3, plain, [-(rcenter(vd1055, 110 ^ []))], clausify('qu(theu(the(211), 1), imp(the(211)))')).
% 29.31/29.33 cnf(4, plain, [110 ^ [] = vd1061], clausify('qu(theu(the(211), 1), imp(the(211)))')).
% 29.31/29.33 cnf(5, plain, [-(ron(vd1057, vd1061))], clausify('and(pred(comma_conjunct2(the(211)), 0), and(pred(comma_conjunct1(the(211)), 0), pred(the(211), 0)))')).
% 29.31/29.33 cnf(6, plain, [-(rcenter(vd1055, vd1061))], clausify('and(pred(comma_conjunct2(the(211)), 0), and(pred(comma_conjunct1(the(211)), 0), pred(the(211), 0)))')).
% 29.31/29.33 cnf(7, plain, [-(vd1057 = vd1058)], clausify('and(pred(conjunct2(210), 4), and(holds(conjunct2(210), 1059, 0), and(pred(conjunct2(210), 1), and(pred(conjunct1(210), 2), pred(conjunct1(210), 1)))))')).
% 29.31/29.33 cnf(8, plain, [-(rpoint(vd1058))], clausify('and(pred(conjunct2(210), 4), and(holds(conjunct2(210), 1059, 0), and(pred(conjunct2(210), 1), and(pred(conjunct1(210), 2), pred(conjunct1(210), 1)))))')).
% 29.31/29.33 cnf(9, plain, [17 ^ [_194858, _194757, _194655, _194552, _194448, _194343], ron(_194757, _194655), _194757 = _194858, rpoint(_194858), rcenter(_194552, _194655), _194343 = _194448, rpoint(_194448)], clausify('qu(cond(axiom(184), 0), imp(cond(axiom(184), 0)))')).
% 29.31/29.33 cnf(10, plain, [-(_196046 = _196165), vf(_195926, _195683) = vf(_195926, _195805), ron(_195805, _196165), ron(_195683, _196046), rcenter(_195926, _196165), rcenter(_195926, _196046), rpoint(_196673), _195805 = _196673, _195683 = _196842, rpoint(_196842)], clausify('qu(cond(axiom(182), 0), imp(cond(axiom(182), 0)))')).
% 29.31/29.33
% 29.31/29.33 cnf('1',plain,[-(ron(vd1057, 110 ^ []))],start(2)).
% 29.31/29.33 cnf('1.1',plain,[ron(vd1057, 110 ^ []), -(17 ^ [vd1058, vd1057, 110 ^ [], vd1055, vd1058, vd1057]), -(vf(vd1055, vd1057) = vf(vd1055, vd1057))],extension(1,bind([[_194858, _194655, _194448, _194343, _194552, _194757], [vd1058, 110 ^ [], vd1058, vd1057, vd1055, vd1057]]))).
% 29.31/29.33 cnf('1.1.1',plain,[17 ^ [vd1058, vd1057, 110 ^ [], vd1055, vd1058, vd1057], ron(vd1057, 110 ^ []), vd1057 = vd1058, rpoint(vd1058), rcenter(vd1055, 110 ^ []), vd1057 = vd1058, rpoint(vd1058)],extension(9,bind([[_194757, _194858, _194552, _194655, _194343, _194448], [vd1057, vd1058, vd1055, 110 ^ [], vd1057, vd1058]]))).
% 29.31/29.33 cnf('1.1.1.1',plain,[-(ron(vd1057, 110 ^ []))],extension(2)).
% 29.31/29.33 cnf('1.1.1.2',plain,[-(vd1057 = vd1058)],extension(7)).
% 29.31/29.33 cnf('1.1.1.3',plain,[-(rpoint(vd1058))],extension(8)).
% 29.31/29.33 cnf('1.1.1.4',plain,[-(rcenter(vd1055, 110 ^ []))],extension(3)).
% 29.31/29.33 cnf('1.1.1.5',plain,[-(vd1057 = vd1058)],extension(7)).
% 29.31/29.33 cnf('1.1.1.6',plain,[-(rpoint(vd1058))],extension(8)).
% 29.31/29.33 cnf('1.1.2',plain,[vf(vd1055, vd1057) = vf(vd1055, vd1057), -(110 ^ [] = vd1061), ron(vd1057, vd1061), ron(vd1057, 110 ^ []), rcenter(vd1055, vd1061), rcenter(vd1055, 110 ^ []), rpoint(vd1058), vd1057 = vd1058, vd1057 = vd1058, rpoint(vd1058)],extension(10,bind([[_196165, _195926, _196046, _195805, _196673, _195683, _196842], [vd1061, vd1055, 110 ^ [], vd1057, vd1058, vd1057, vd1058]]))).
% 29.31/29.33 cnf('1.1.2.1',plain,[110 ^ [] = vd1061],extension(4)).
% 29.31/29.33 cnf('1.1.2.2',plain,[-(ron(vd1057, vd1061))],extension(5)).
% 29.31/29.33 cnf('1.1.2.3',plain,[-(ron(vd1057, 110 ^ []))],extension(2)).
% 29.31/29.33 cnf('1.1.2.4',plain,[-(rcenter(vd1055, vd1061))],extension(6)).
% 29.31/29.33 cnf('1.1.2.5',plain,[-(rcenter(vd1055, 110 ^ []))],extension(3)).
% 29.31/29.33 cnf('1.1.2.6',plain,[-(rpoint(vd1058))],extension(8)).
% 29.31/29.33 cnf('1.1.2.7',plain,[-(vd1057 = vd1058)],extension(7)).
% 29.31/29.33 cnf('1.1.2.8',plain,[-(vd1057 = vd1058)],extension(7)).
% 29.31/29.33 cnf('1.1.2.9',plain,[-(rpoint(vd1058))],extension(8)).
% 29.31/29.33 %-----------------------------------------------------
% 29.31/29.33
% 29.31/29.33 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------