%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GEO308+1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n004.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:30 EDT 2022
% Result : Theorem 140.07s 135.54s
% Output : Proof 140.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GEO308+1 : TPTP v8.1.0. Released v4.1.0.
% 0.03/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n004.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Fri Jun 17 20:14:53 EDT 2022
% 0.13/0.34 % CPUTime :
% 140.07/135.54 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 140.07/135.54 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 140.07/135.55
% 140.07/135.55 %-----------------------------------------------------
% 140.07/135.55 fof('holds(358, 1317, 0)', conjecture, vangle(vd1288, vd1287, vd1289) = vangle(vd1299, vd1287, vd1289), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'holds(358, 1317, 0)')).
% 140.07/135.55 fof('neg(neg(356))', axiom, ~ rR(vd1287, vd1288, vd1299), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'neg(neg(356))')).
% 140.07/135.55 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 & ? [_203357] : (vd1289 = _203357 & rpoint(_203357)) & ? [_203378] : (vd1288 = _203378 & rpoint(_203378)) & ? [_203399] : (vd1287 = _203399 & rpoint(_203399)), file('/export/starexec/sandbox2/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.07/135.55 fof('qu(cond(axiom(194), 0), imp(cond(axiom(194), 0)))', axiom, ! [_203820, _203823, _203826, _203829, _203832, _203835, _203838] : (~ rR(_203820, _203826, _203832) & ~ rR(_203820, _203823, _203829) & (! _203832) = _203820 & (! _203829) = _203820 & (! _203826) = _203820 & (! _203823) = _203820 & ron(_203832, _203838) & ron(_203826, _203838) & ron(_203829, _203835) & ron(_203823, _203835) & ron(_203820, _203835) & ? [_203958] : (_203838 = _203958 & rline(_203958)) & ? [_203979] : (_203835 = _203979 & rline(_203979)) & ? [_204000] : (_203832 = _204000 & rpoint(_204000)) & ? [_204021] : (_203829 = _204021 & rpoint(_204021)) & ? [_204042] : (_203826 = _204042 & rpoint(_204042)) & ? [_204063] : (_203823 = _204063 & rpoint(_204063)) & ? [_204084] : (_203820 = _204084 & rpoint(_204084)) => vangle(_203823, _203820, _203826) = vangle(_203829, _203820, _203832)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'qu(cond(axiom(194), 0), imp(cond(axiom(194), 0)))')).
% 140.07/135.55 fof('pred(348, 4)', axiom, vd1299 = vd1300, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'pred(348, 4)')).
% 140.07/135.55 fof('pred(348, 1)', axiom, rpoint(vd1300), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'pred(348, 1)')).
% 140.07/135.55 fof('holds(conjunct1(conjunct2(conjunct2(355))), 1311, 0)', axiom, (! vd1299) = vd1287, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'holds(conjunct1(conjunct2(conjunct2(355))), 1311, 0)')).
% 140.07/135.55 fof('holds(conjunct1(conjunct2(355)), 1313, 0)', axiom, (! vd1289) = vd1287, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'holds(conjunct1(conjunct2(355)), 1313, 0)')).
% 140.07/135.55 fof('pred(conjunct1(349), 0)', axiom, ron(vd1299, vd1295), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'pred(conjunct1(349), 0)')).
% 140.07/135.55 fof('pred(s2(plural(347)), 0)', axiom, ron(vd1289, vd1297), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'pred(s2(plural(347)), 0)')).
% 140.07/135.55 fof('pred(347, 0)', axiom, rline(vd1297), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'pred(347, 0)')).
% 140.07/135.55 fof('pred(s2(plural(346)), 0)', axiom, ron(vd1288, vd1295), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'pred(s2(plural(346)), 0)')).
% 140.07/135.55 fof('pred(s1(plural(346)), 0)', axiom, ron(vd1287, vd1295), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'pred(s1(plural(346)), 0)')).
% 140.07/135.55 fof('pred(346, 0)', axiom, rline(vd1295), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'pred(346, 0)')).
% 140.07/135.55 fof('qu(cond(axiom(93), 0), imp(cond(axiom(93), 0)))', axiom, ! [_205514, _205517, _205520, _205523] : (rR(_205517, _205514, _205523) & rR(_205517, _205514, _205520) & ? [_205557] : (_205523 = _205557 & rpoint(_205557)) & ? [_205578] : (_205520 = _205578 & rpoint(_205578)) & ? [_205599] : (_205517 = _205599 & rpoint(_205599)) & ? [_205620] : (_205514 = _205620 & rpoint(_205620)) => ~ rR(_205517, _205520, _205523)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'qu(cond(axiom(93), 0), imp(cond(axiom(93), 0)))')).
% 140.07/135.55
% 140.07/135.55 cnf(1, plain, [vangle(vd1288, vd1287, vd1289) = vangle(vd1299, vd1287, vd1289)], clausify('holds(358, 1317, 0)')).
% 140.07/135.55 cnf(2, plain, [-(_16076 = _16076)], theory(equality)).
% 140.07/135.55 cnf(3, plain, [_16082 = _16083, -(_16083 = _16082)], theory(equality)).
% 140.07/135.55 cnf(4, plain, [rR(vd1287, vd1288, vd1299)], clausify('neg(neg(356))')).
% 140.07/135.55 cnf(5, 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.07/135.55 cnf(6, 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.07/135.55 cnf(7, 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.07/135.55 cnf(8, 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.07/135.55 cnf(9, 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.07/135.55 cnf(10, 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.07/135.55 cnf(11, 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.07/135.55 cnf(12, 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.07/135.55 cnf(13, plain, [-(vangle(_16675, _16674, _16676) = vangle(_16677, _16674, _16678)), -(rR(_16674, _16676, _16678)), -(rR(_16674, _16675, _16677)), -(_16678 = _16674), -(_16677 = _16674), -(_16676 = _16674), -(_16675 = _16674), ron(_16678, _16680), ron(_16676, _16680), ron(_16677, _16679), ron(_16675, _16679), ron(_16674, _16679), rline(_16716), _16680 = _16716, rline(_16722), _16679 = _16722, rpoint(_16728), _16678 = _16728, rpoint(_16734), _16677 = _16734, rpoint(_16740), _16676 = _16740, rpoint(_16746), _16675 = _16746, _16674 = _16752, rpoint(_16752)], clausify('qu(cond(axiom(194), 0), imp(cond(axiom(194), 0)))')).
% 140.07/135.55 cnf(14, plain, [-(vd1299 = vd1300)], clausify('pred(348, 4)')).
% 140.07/135.55 cnf(15, plain, [-(rpoint(vd1300))], clausify('pred(348, 1)')).
% 140.07/135.55 cnf(16, plain, [vd1299 = vd1287], clausify('holds(conjunct1(conjunct2(conjunct2(355))), 1311, 0)')).
% 140.07/135.55 cnf(17, plain, [vd1289 = vd1287], clausify('holds(conjunct1(conjunct2(355)), 1313, 0)')).
% 140.07/135.55 cnf(18, plain, [-(ron(vd1299, vd1295))], clausify('pred(conjunct1(349), 0)')).
% 140.07/135.55 cnf(19, plain, [-(ron(vd1289, vd1297))], clausify('pred(s2(plural(347)), 0)')).
% 140.07/135.55 cnf(20, plain, [-(rline(vd1297))], clausify('pred(347, 0)')).
% 140.07/135.55 cnf(21, plain, [-(ron(vd1288, vd1295))], clausify('pred(s2(plural(346)), 0)')).
% 140.07/135.55 cnf(22, plain, [-(ron(vd1287, vd1295))], clausify('pred(s1(plural(346)), 0)')).
% 140.07/135.55 cnf(23, plain, [-(rline(vd1295))], clausify('pred(346, 0)')).
% 140.07/135.55 cnf(24, plain, [rR(_19779, _19780, _19781), rR(_19779, _19778, _19781), rR(_19779, _19778, _19780), rpoint(_19790), _19781 = _19790, rpoint(_19796), _19780 = _19796, rpoint(_19802), _19779 = _19802, _19778 = _19808, rpoint(_19808)], clausify('qu(cond(axiom(93), 0), imp(cond(axiom(93), 0)))')).
% 140.07/135.55
% 140.07/135.55 cnf('1',plain,[vangle(vd1288, vd1287, vd1289) = vangle(vd1299, vd1287, vd1289)],start(1)).
% 140.07/135.55 cnf('1.1',plain,[-(vangle(vd1288, vd1287, vd1289) = vangle(vd1299, vd1287, vd1289)), -(rR(vd1287, vd1289, vd1289)), -(rR(vd1287, vd1288, vd1299)), -(vd1289 = vd1287), -(vd1299 = vd1287), -(vd1289 = vd1287), -(vd1288 = vd1287), ron(vd1289, vd1297), ron(vd1289, vd1297), ron(vd1299, vd1295), ron(vd1288, vd1295), ron(vd1287, vd1295), rline(vd1297), vd1297 = vd1297, rline(vd1295), vd1295 = vd1295, rpoint(1 ^ []), vd1289 = 1 ^ [], rpoint(vd1300), vd1299 = vd1300, rpoint(1 ^ []), vd1289 = 1 ^ [], rpoint(2 ^ []), vd1288 = 2 ^ [], vd1287 = 3 ^ [], rpoint(3 ^ [])],extension(13,bind([[_16680, _16716, _16679, _16722, _16678, _16728, _16677, _16734, _16676, _16740, _16675, _16746, _16674, _16752], [vd1297, vd1297, vd1295, vd1295, vd1289, 1 ^ [], vd1299, vd1300, vd1289, 1 ^ [], vd1288, 2 ^ [], vd1287, 3 ^ []]]))).
% 140.07/135.55 cnf('1.1.1',plain,[rR(vd1287, vd1289, vd1289), rR(vd1287, vd1289, vd1289), rR(vd1287, vd1289, vd1289), rpoint(1 ^ []), vd1289 = 1 ^ [], rpoint(1 ^ []), vd1289 = 1 ^ [], rpoint(3 ^ []), vd1287 = 3 ^ [], vd1289 = 1 ^ [], rpoint(1 ^ [])],extension(24,bind([[_19781, _19790, _19780, _19796, _19779, _19802, _19778, _19808], [vd1289, 1 ^ [], vd1289, 1 ^ [], vd1287, 3 ^ [], vd1289, 1 ^ []]]))).
% 140.07/135.55 cnf('1.1.1.1',plain,[-(rR(vd1287, vd1289, vd1289))],reduction('1.1')).
% 140.07/135.55 cnf('1.1.1.2',plain,[-(rR(vd1287, vd1289, vd1289))],lemmata('1.1.1')).
% 140.07/135.55 cnf('1.1.1.3',plain,[-(rpoint(1 ^ []))],extension(8)).
% 140.07/135.55 cnf('1.1.1.4',plain,[-(vd1289 = 1 ^ [])],extension(7)).
% 140.07/135.55 cnf('1.1.1.5',plain,[-(rpoint(1 ^ []))],extension(8)).
% 140.07/135.55 cnf('1.1.1.6',plain,[-(vd1289 = 1 ^ [])],extension(7)).
% 140.07/135.55 cnf('1.1.1.7',plain,[-(rpoint(3 ^ []))],extension(12)).
% 140.07/135.55 cnf('1.1.1.8',plain,[-(vd1287 = 3 ^ [])],extension(11)).
% 140.07/135.55 cnf('1.1.1.9',plain,[-(vd1289 = 1 ^ [])],extension(7)).
% 140.07/135.55 cnf('1.1.1.10',plain,[-(rpoint(1 ^ []))],extension(8)).
% 140.07/135.55 cnf('1.1.2',plain,[rR(vd1287, vd1288, vd1299)],extension(4)).
% 140.07/135.55 cnf('1.1.3',plain,[vd1289 = vd1287, -(vd1287 = vd1289)],extension(3,bind([[_16083, _16082], [vd1287, vd1289]]))).
% 140.07/135.55 cnf('1.1.3.1',plain,[vd1287 = vd1289],extension(5)).
% 140.07/135.55 cnf('1.1.4',plain,[vd1299 = vd1287],extension(16)).
% 140.07/135.55 cnf('1.1.5',plain,[vd1289 = vd1287],extension(17)).
% 140.07/135.55 cnf('1.1.6',plain,[vd1288 = vd1287, -(vd1287 = vd1288)],extension(3,bind([[_16083, _16082], [vd1287, vd1288]]))).
% 140.07/135.55 cnf('1.1.6.1',plain,[vd1287 = vd1288],extension(6)).
% 140.07/135.55 cnf('1.1.7',plain,[-(ron(vd1289, vd1297))],extension(19)).
% 140.07/135.55 cnf('1.1.8',plain,[-(ron(vd1289, vd1297))],extension(19)).
% 140.07/135.55 cnf('1.1.9',plain,[-(ron(vd1299, vd1295))],extension(18)).
% 140.07/135.55 cnf('1.1.10',plain,[-(ron(vd1288, vd1295))],extension(21)).
% 140.07/135.55 cnf('1.1.11',plain,[-(ron(vd1287, vd1295))],extension(22)).
% 140.07/135.55 cnf('1.1.12',plain,[-(rline(vd1297))],extension(20)).
% 140.07/135.55 cnf('1.1.13',plain,[-(vd1297 = vd1297)],extension(2,bind([[_16076], [vd1297]]))).
% 140.07/135.55 cnf('1.1.14',plain,[-(rline(vd1295))],extension(23)).
% 140.07/135.55 cnf('1.1.15',plain,[-(vd1295 = vd1295)],extension(2,bind([[_16076], [vd1295]]))).
% 140.07/135.55 cnf('1.1.16',plain,[-(rpoint(1 ^ []))],extension(8)).
% 140.07/135.55 cnf('1.1.17',plain,[-(vd1289 = 1 ^ [])],extension(7)).
% 140.07/135.55 cnf('1.1.18',plain,[-(rpoint(vd1300))],extension(15)).
% 140.07/135.55 cnf('1.1.19',plain,[-(vd1299 = vd1300)],extension(14)).
% 140.07/135.55 cnf('1.1.20',plain,[-(rpoint(1 ^ []))],extension(8)).
% 140.07/135.55 cnf('1.1.21',plain,[-(vd1289 = 1 ^ [])],extension(7)).
% 140.07/135.55 cnf('1.1.22',plain,[-(rpoint(2 ^ []))],extension(10)).
% 140.07/135.55 cnf('1.1.23',plain,[-(vd1288 = 2 ^ [])],extension(9)).
% 140.07/135.55 cnf('1.1.24',plain,[-(vd1287 = 3 ^ [])],extension(11)).
% 140.07/135.55 cnf('1.1.25',plain,[-(rpoint(3 ^ []))],extension(12)).
% 140.07/135.55 %-----------------------------------------------------
% 140.07/135.55
% 140.07/135.56 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------