%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GEO321+1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n025.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:33 EDT 2022
% Result : Theorem 140.26s 135.98s
% Output : Proof 140.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO321+1 : TPTP v8.1.0. Released v4.1.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n025.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 : Sat Jun 18 18:39:43 EDT 2022
% 0.12/0.34 % CPUTime :
% 140.26/135.98 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 140.26/135.99 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 140.26/136.00
% 140.26/136.00 %-----------------------------------------------------
% 140.26/136.00 fof('holds(374, 1342, 0)', conjecture, vangle(vd1289, vd1287, vd1288) = vangle(vd1302, vd1287, vd1288), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'holds(374, 1342, 0)')).
% 140.26/136.00 fof('neg(neg(372))', axiom, ~ rR(vd1287, vd1289, vd1302), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'neg(neg(372))')).
% 140.26/136.00 fof('and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))', axiom, vd1302 = vd1303 & rR(vd1289, vd1287, vd1302) & rpoint(vd1303) & rR(vd1288, vd1287, vd1299), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))')).
% 140.26/136.00 fof('and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))', axiom, vf(vd1287, vd1288) = vf(vd1287, vd1289) & (! vd1288) = vd1289 & (! vd1287) = vd1289 & (! vd1287) = vd1288 & ? [_241653] : (vd1289 = _241653 & rpoint(_241653)) & ? [_241674] : (vd1288 = _241674 & rpoint(_241674)) & ? [_241695] : (vd1287 = _241695 & rpoint(_241695)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))')).
% 140.26/136.00 fof('qu(cond(axiom(194), 0), imp(cond(axiom(194), 0)))', axiom, ! [_242116, _242119, _242122, _242125, _242128, _242131, _242134] : (~ rR(_242116, _242122, _242128) & ~ rR(_242116, _242119, _242125) & (! _242128) = _242116 & (! _242125) = _242116 & (! _242122) = _242116 & (! _242119) = _242116 & ron(_242128, _242134) & ron(_242122, _242134) & ron(_242125, _242131) & ron(_242119, _242131) & ron(_242116, _242131) & ? [_242254] : (_242134 = _242254 & rline(_242254)) & ? [_242275] : (_242131 = _242275 & rline(_242275)) & ? [_242296] : (_242128 = _242296 & rpoint(_242296)) & ? [_242317] : (_242125 = _242317 & rpoint(_242317)) & ? [_242338] : (_242122 = _242338 & rpoint(_242338)) & ? [_242359] : (_242119 = _242359 & rpoint(_242359)) & ? [_242380] : (_242116 = _242380 & rpoint(_242380)) => vangle(_242119, _242116, _242122) = vangle(_242125, _242116, _242128)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'qu(cond(axiom(194), 0), imp(cond(axiom(194), 0)))')).
% 140.26/136.00 fof('holds(conjunct1(conjunct2(conjunct2(371))), 1334, 0)', axiom, (! vd1302) = vd1287, file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'holds(conjunct1(conjunct2(conjunct2(371))), 1334, 0)')).
% 140.26/136.00 fof('holds(conjunct1(371), 1337, 0)', axiom, (! vd1288) = vd1287, file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'holds(conjunct1(371), 1337, 0)')).
% 140.26/136.00 fof('pred(s3(plural(370)), 0)', axiom, ron(vd1288, vd1295), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'pred(s3(plural(370)), 0)')).
% 140.26/136.00 fof('pred(conjunct2(349), 0)', axiom, ron(vd1302, vd1297), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'pred(conjunct2(349), 0)')).
% 140.26/136.00 fof('pred(s2(plural(347)), 0)', axiom, ron(vd1289, vd1297), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'pred(s2(plural(347)), 0)')).
% 140.26/136.00 fof('pred(s1(plural(347)), 0)', axiom, ron(vd1287, vd1297), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'pred(s1(plural(347)), 0)')).
% 140.26/136.00 fof('pred(347, 0)', axiom, rline(vd1297), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'pred(347, 0)')).
% 140.26/136.00 fof('pred(346, 0)', axiom, rline(vd1295), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'pred(346, 0)')).
% 140.26/136.00 fof('qu(cond(axiom(93), 0), imp(cond(axiom(93), 0)))', axiom, ! [_243751, _243754, _243757, _243760] : (rR(_243754, _243751, _243760) & rR(_243754, _243751, _243757) & ? [_243794] : (_243760 = _243794 & rpoint(_243794)) & ? [_243815] : (_243757 = _243815 & rpoint(_243815)) & ? [_243836] : (_243754 = _243836 & rpoint(_243836)) & ? [_243857] : (_243751 = _243857 & rpoint(_243857)) => ~ rR(_243754, _243757, _243760)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'qu(cond(axiom(93), 0), imp(cond(axiom(93), 0)))')).
% 140.26/136.00
% 140.26/136.00 cnf(1, plain, [vangle(vd1289, vd1287, vd1288) = vangle(vd1302, vd1287, vd1288)], clausify('holds(374, 1342, 0)')).
% 140.26/136.00 cnf(2, plain, [-(_16987 = _16987)], theory(equality)).
% 140.26/136.00 cnf(3, plain, [_16993 = _16994, -(_16994 = _16993)], theory(equality)).
% 140.26/136.00 cnf(4, plain, [rR(vd1287, vd1289, vd1302)], clausify('neg(neg(372))')).
% 140.26/136.00 cnf(5, plain, [-(vd1302 = vd1303)], clausify('and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))')).
% 140.26/136.00 cnf(6, plain, [-(rpoint(vd1303))], clausify('and(pred(conjunct2(348), 4), and(holds(conjunct2(348), 1304, 0), and(pred(conjunct2(348), 1), holds(conjunct1(348), 1301, 0))))')).
% 140.26/136.00 cnf(7, plain, [vd1287 = vd1289], clausify('and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))')).
% 140.26/136.00 cnf(8, plain, [vd1287 = vd1288], clausify('and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))')).
% 140.26/136.00 cnf(9, plain, [-(vd1289 = 1 ^ [])], clausify('and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))')).
% 140.26/136.00 cnf(10, plain, [-(rpoint(1 ^ []))], clausify('and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))')).
% 140.26/136.00 cnf(11, plain, [-(vd1288 = 2 ^ [])], clausify('and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))')).
% 140.26/136.00 cnf(12, plain, [-(rpoint(2 ^ []))], clausify('and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))')).
% 140.26/136.00 cnf(13, plain, [-(vd1287 = 3 ^ [])], clausify('and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))')).
% 140.26/136.00 cnf(14, plain, [-(rpoint(3 ^ []))], clausify('and(holds(conjunct2(345), 1294, 0), and(pred(conjunct1(345), 9), and(pred(conjunct1(345), 8), and(pred(conjunct1(345), 7), and(qe(s3(plural(345))), and(qe(s2(plural(345))), qe(s1(plural(345)))))))))')).
% 140.26/136.00 cnf(15, plain, [-(vangle(_17597, _17596, _17598) = vangle(_17599, _17596, _17600)), -(rR(_17596, _17598, _17600)), -(rR(_17596, _17597, _17599)), -(_17600 = _17596), -(_17599 = _17596), -(_17598 = _17596), -(_17597 = _17596), ron(_17600, _17602), ron(_17598, _17602), ron(_17599, _17601), ron(_17597, _17601), ron(_17596, _17601), rline(_17650), _17602 = _17650, rline(_17656), _17601 = _17656, rpoint(_17662), _17600 = _17662, rpoint(_17668), _17599 = _17668, rpoint(_17674), _17598 = _17674, rpoint(_17680), _17597 = _17680, _17596 = _17686, rpoint(_17686)], clausify('qu(cond(axiom(194), 0), imp(cond(axiom(194), 0)))')).
% 140.26/136.00 cnf(16, plain, [vd1302 = vd1287], clausify('holds(conjunct1(conjunct2(conjunct2(371))), 1334, 0)')).
% 140.26/136.00 cnf(17, plain, [vd1288 = vd1287], clausify('holds(conjunct1(371), 1337, 0)')).
% 140.26/136.00 cnf(18, plain, [-(ron(vd1288, vd1295))], clausify('pred(s3(plural(370)), 0)')).
% 140.26/136.00 cnf(19, plain, [-(ron(vd1302, vd1297))], clausify('pred(conjunct2(349), 0)')).
% 140.26/136.00 cnf(20, plain, [-(ron(vd1289, vd1297))], clausify('pred(s2(plural(347)), 0)')).
% 140.26/136.00 cnf(21, plain, [-(ron(vd1287, vd1297))], clausify('pred(s1(plural(347)), 0)')).
% 140.26/136.00 cnf(22, plain, [-(rline(vd1297))], clausify('pred(347, 0)')).
% 140.26/136.00 cnf(23, plain, [-(rline(vd1295))], clausify('pred(346, 0)')).
% 140.26/136.00 cnf(24, plain, [rR(_21408, _21409, _21410), rR(_21408, _21407, _21410), rR(_21408, _21407, _21409), rpoint(_21419), _21410 = _21419, rpoint(_21425), _21409 = _21425, rpoint(_21431), _21408 = _21431, _21407 = _21437, rpoint(_21437)], clausify('qu(cond(axiom(93), 0), imp(cond(axiom(93), 0)))')).
% 140.26/136.00
% 140.26/136.00 cnf('1',plain,[vangle(vd1289, vd1287, vd1288) = vangle(vd1302, vd1287, vd1288)],start(1)).
% 140.26/136.00 cnf('1.1',plain,[-(vangle(vd1289, vd1287, vd1288) = vangle(vd1302, vd1287, vd1288)), -(rR(vd1287, vd1288, vd1288)), -(rR(vd1287, vd1289, vd1302)), -(vd1288 = vd1287), -(vd1302 = vd1287), -(vd1288 = vd1287), -(vd1289 = vd1287), ron(vd1288, vd1295), ron(vd1288, vd1295), ron(vd1302, vd1297), ron(vd1289, vd1297), ron(vd1287, vd1297), rline(vd1295), vd1295 = vd1295, rline(vd1297), vd1297 = vd1297, rpoint(2 ^ []), vd1288 = 2 ^ [], rpoint(vd1303), vd1302 = vd1303, rpoint(2 ^ []), vd1288 = 2 ^ [], rpoint(1 ^ []), vd1289 = 1 ^ [], vd1287 = 3 ^ [], rpoint(3 ^ [])],extension(15,bind([[_17602, _17650, _17601, _17656, _17600, _17662, _17599, _17668, _17598, _17674, _17597, _17680, _17596, _17686], [vd1295, vd1295, vd1297, vd1297, vd1288, 2 ^ [], vd1302, vd1303, vd1288, 2 ^ [], vd1289, 1 ^ [], vd1287, 3 ^ []]]))).
% 140.26/136.00 cnf('1.1.1',plain,[rR(vd1287, vd1288, vd1288), rR(vd1287, vd1288, vd1288), rR(vd1287, vd1288, vd1288), rpoint(2 ^ []), vd1288 = 2 ^ [], rpoint(2 ^ []), vd1288 = 2 ^ [], rpoint(3 ^ []), vd1287 = 3 ^ [], vd1288 = 2 ^ [], rpoint(2 ^ [])],extension(24,bind([[_21410, _21419, _21409, _21425, _21408, _21431, _21407, _21437], [vd1288, 2 ^ [], vd1288, 2 ^ [], vd1287, 3 ^ [], vd1288, 2 ^ []]]))).
% 140.26/136.00 cnf('1.1.1.1',plain,[-(rR(vd1287, vd1288, vd1288))],reduction('1.1')).
% 140.26/136.00 cnf('1.1.1.2',plain,[-(rR(vd1287, vd1288, vd1288))],lemmata('1.1.1')).
% 140.26/136.00 cnf('1.1.1.3',plain,[-(rpoint(2 ^ []))],extension(12)).
% 140.26/136.00 cnf('1.1.1.4',plain,[-(vd1288 = 2 ^ [])],extension(11)).
% 140.26/136.00 cnf('1.1.1.5',plain,[-(rpoint(2 ^ []))],extension(12)).
% 140.26/136.00 cnf('1.1.1.6',plain,[-(vd1288 = 2 ^ [])],extension(11)).
% 140.26/136.00 cnf('1.1.1.7',plain,[-(rpoint(3 ^ []))],extension(14)).
% 140.26/136.00 cnf('1.1.1.8',plain,[-(vd1287 = 3 ^ [])],extension(13)).
% 140.26/136.00 cnf('1.1.1.9',plain,[-(vd1288 = 2 ^ [])],extension(11)).
% 140.26/136.00 cnf('1.1.1.10',plain,[-(rpoint(2 ^ []))],extension(12)).
% 140.26/136.00 cnf('1.1.2',plain,[rR(vd1287, vd1289, vd1302)],extension(4)).
% 140.26/136.00 cnf('1.1.3',plain,[vd1288 = vd1287, -(vd1287 = vd1288)],extension(3,bind([[_16994, _16993], [vd1287, vd1288]]))).
% 140.26/136.00 cnf('1.1.3.1',plain,[vd1287 = vd1288],extension(8)).
% 140.26/136.00 cnf('1.1.4',plain,[vd1302 = vd1287],extension(16)).
% 140.26/136.00 cnf('1.1.5',plain,[vd1288 = vd1287],extension(17)).
% 140.26/136.00 cnf('1.1.6',plain,[vd1289 = vd1287, -(vd1287 = vd1289)],extension(3,bind([[_16994, _16993], [vd1287, vd1289]]))).
% 140.26/136.00 cnf('1.1.6.1',plain,[vd1287 = vd1289],extension(7)).
% 140.26/136.00 cnf('1.1.7',plain,[-(ron(vd1288, vd1295))],extension(18)).
% 140.26/136.00 cnf('1.1.8',plain,[-(ron(vd1288, vd1295))],extension(18)).
% 140.26/136.00 cnf('1.1.9',plain,[-(ron(vd1302, vd1297))],extension(19)).
% 140.26/136.00 cnf('1.1.10',plain,[-(ron(vd1289, vd1297))],extension(20)).
% 140.26/136.00 cnf('1.1.11',plain,[-(ron(vd1287, vd1297))],extension(21)).
% 140.26/136.00 cnf('1.1.12',plain,[-(rline(vd1295))],extension(23)).
% 140.26/136.00 cnf('1.1.13',plain,[-(vd1295 = vd1295)],extension(2,bind([[_16987], [vd1295]]))).
% 140.26/136.00 cnf('1.1.14',plain,[-(rline(vd1297))],extension(22)).
% 140.26/136.00 cnf('1.1.15',plain,[-(vd1297 = vd1297)],extension(2,bind([[_16987], [vd1297]]))).
% 140.26/136.00 cnf('1.1.16',plain,[-(rpoint(2 ^ []))],extension(12)).
% 140.26/136.00 cnf('1.1.17',plain,[-(vd1288 = 2 ^ [])],extension(11)).
% 140.26/136.00 cnf('1.1.18',plain,[-(rpoint(vd1303))],extension(6)).
% 140.26/136.00 cnf('1.1.19',plain,[-(vd1302 = vd1303)],extension(5)).
% 140.26/136.00 cnf('1.1.20',plain,[-(rpoint(2 ^ []))],extension(12)).
% 140.26/136.00 cnf('1.1.21',plain,[-(vd1288 = 2 ^ [])],extension(11)).
% 140.26/136.00 cnf('1.1.22',plain,[-(rpoint(1 ^ []))],extension(10)).
% 140.26/136.00 cnf('1.1.23',plain,[-(vd1289 = 1 ^ [])],extension(9)).
% 140.26/136.00 cnf('1.1.24',plain,[-(vd1287 = 3 ^ [])],extension(13)).
% 140.26/136.00 cnf('1.1.25',plain,[-(rpoint(3 ^ []))],extension(14)).
% 140.26/136.00 %-----------------------------------------------------
% 140.26/136.00
% 140.26/136.00 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------