%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GEO286+1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n005.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:24 EDT 2022
% Result : Theorem 130.12s 126.00s
% Output : Proof 130.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GEO286+1 : TPTP v8.1.0. Released v4.1.0.
% 0.03/0.13 % Command : leancop_casc.sh %s %d
% 0.13/0.34 % Computer : n005.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 : Sat Jun 18 02:32:53 EDT 2022
% 0.13/0.35 % CPUTime :
% 130.12/126.00 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 130.12/126.01 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 130.12/126.01
% 130.12/126.01 %-----------------------------------------------------
% 130.12/126.01 fof('qe(261)', conjecture, ? [_159349] : (rR(_159349, vd1123, vd1125) & ron(_159349, vd1152) & ron(_159349, vd1151) & rpoint(_159349)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'qe(261)')).
% 130.12/126.01 fof('neg(neg(comma_conjunct2(260)))', axiom, ~ ron(vd1125, vd1152), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'neg(neg(comma_conjunct2(260)))')).
% 130.12/126.01 fof('neg(neg(260))', axiom, ~ rinside(vd1125, vd1152), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'neg(neg(260))')).
% 130.12/126.01 fof('and(and(pred(comma_conjunct2(comma_conjunct2(comma_conjunct2(259))), 0), and(pred(comma_conjunct1(comma_conjunct2(comma_conjunct2(259))), 0), and(pred(comma_conjunct2(comma_conjunct2(259)), 0), pred(comma_conjunct1(comma_conjunct2(259)), 0)))), pred(comma_conjunct1(259), 0))', axiom, ron(vd1127, vd1152) & rcenter(vd1123, vd1152) & rcircle(vd1152) & ron(vd1125, vd1151) & ron(vd1123, vd1151), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'and(and(pred(comma_conjunct2(comma_conjunct2(comma_conjunct2(259))), 0), and(pred(comma_conjunct1(comma_conjunct2(comma_conjunct2(259))), 0), and(pred(comma_conjunct2(comma_conjunct2(259)), 0), pred(comma_conjunct1(comma_conjunct2(259)), 0)))), pred(comma_conjunct1(259), 0))')).
% 130.12/126.01 fof('holds(258, 1150, 0)', axiom, vd1123 = vd1129, file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'holds(258, 1150, 0)')).
% 130.12/126.01 fof('and(and(and(and(holds(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(242)))))), 1133, 0), and(holds(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(242)))))), 1132, 0), and(holds(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(242))))), 1131, 0), and(pred(conjunct1(conjunct2(conjunct2(conjunct2(242)))), 2), pred(conjunct1(conjunct2(conjunct2(conjunct2(242)))), 1))))), and(pred(conjunct1(conjunct2(conjunct2(242))), 2), pred(conjunct1(conjunct2(conjunct2(242))), 1))), and(pred(conjunct1(conjunct2(242)), 2), pred(conjunct1(conjunct2(242)), 1))), and(pred(conjunct1(242), 2), pred(conjunct1(242), 1)))', axiom, rless(vf(vd1127, vd1129), vf(vd1123, vd1125)) & (! vd1127) = vd1129 & (! vd1123) = vd1125 & vd1129 = vd1130 & rpoint(vd1130) & vd1127 = vd1128 & rpoint(vd1128) & vd1125 = vd1126 & rpoint(vd1126) & vd1123 = vd1124 & rpoint(vd1124), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'and(and(and(and(holds(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(242)))))), 1133, 0), and(holds(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(242)))))), 1132, 0), and(holds(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(242))))), 1131, 0), and(pred(conjunct1(conjunct2(conjunct2(conjunct2(242)))), 2), pred(conjunct1(conjunct2(conjunct2(conjunct2(242)))), 1))))), and(pred(conjunct1(conjunct2(conjunct2(242))), 2), pred(conjunct1(conjunct2(conjunct2(242))), 1))), and(pred(conjunct1(conjunct2(242)), 2), pred(conjunct1(conjunct2(242)), 1))), and(pred(conjunct1(242), 2), pred(conjunct1(242), 1)))')).
% 130.12/126.01 fof('pred(259, 0)', axiom, rline(vd1151), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'pred(259, 0)')).
% 130.12/126.01 fof('qu(cond(axiom(61), 0), imp(cond(axiom(61), 0)))', axiom, ! [_160101, _160104, _160107, _160110, _160113, _160116, _160119, _160122] : (ron(_160119, _160107) & ~ ron(_160119, _160101) & ~ rinside(_160119, _160101) & _160119 = _160122 & rpoint(_160122) & ron(_160113, _160107) & rinside(_160113, _160101) & _160113 = _160116 & rpoint(_160116) & _160107 = _160110 & rline(_160110) & _160101 = _160104 & rcircle(_160104) => ? [_160236] : (rR(_160236, _160113, _160119) & ron(_160236, _160101) & ron(_160236, _160107) & rpoint(_160236))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'qu(cond(axiom(61), 0), imp(cond(axiom(61), 0)))')).
% 130.12/126.01 fof('qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))', axiom, ! [_160868, _160871] : (rcenter(_160868, _160871) => rinside(_160868, _160871)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))')).
% 130.12/126.01
% 130.12/126.01 cnf(1, plain, [rR(_19910, vd1123, vd1125), ron(_19910, vd1152), ron(_19910, vd1151), rpoint(_19910)], clausify('qe(261)')).
% 130.12/126.01 cnf(2, plain, [-(_14927 = _14927)], theory(equality)).
% 130.12/126.01 cnf(3, plain, [-(_14943 = _14945), _14943 = _14944, _14944 = _14945], theory(equality)).
% 130.12/126.01 cnf(4, plain, [ron(vd1125, vd1152)], clausify('neg(neg(comma_conjunct2(260)))')).
% 130.12/126.01 cnf(5, plain, [rinside(vd1125, vd1152)], clausify('neg(neg(260))')).
% 130.12/126.01 cnf(6, plain, [-(rcenter(vd1123, vd1152))], clausify('and(and(pred(comma_conjunct2(comma_conjunct2(comma_conjunct2(259))), 0), and(pred(comma_conjunct1(comma_conjunct2(comma_conjunct2(259))), 0), and(pred(comma_conjunct2(comma_conjunct2(259)), 0), pred(comma_conjunct1(comma_conjunct2(259)), 0)))), pred(comma_conjunct1(259), 0))')).
% 130.12/126.01 cnf(7, plain, [-(rcircle(vd1152))], clausify('and(and(pred(comma_conjunct2(comma_conjunct2(comma_conjunct2(259))), 0), and(pred(comma_conjunct1(comma_conjunct2(comma_conjunct2(259))), 0), and(pred(comma_conjunct2(comma_conjunct2(259)), 0), pred(comma_conjunct1(comma_conjunct2(259)), 0)))), pred(comma_conjunct1(259), 0))')).
% 130.12/126.01 cnf(8, plain, [-(ron(vd1125, vd1151))], clausify('and(and(pred(comma_conjunct2(comma_conjunct2(comma_conjunct2(259))), 0), and(pred(comma_conjunct1(comma_conjunct2(comma_conjunct2(259))), 0), and(pred(comma_conjunct2(comma_conjunct2(259)), 0), pred(comma_conjunct1(comma_conjunct2(259)), 0)))), pred(comma_conjunct1(259), 0))')).
% 130.12/126.01 cnf(9, plain, [-(ron(vd1123, vd1151))], clausify('and(and(pred(comma_conjunct2(comma_conjunct2(comma_conjunct2(259))), 0), and(pred(comma_conjunct1(comma_conjunct2(comma_conjunct2(259))), 0), and(pred(comma_conjunct2(comma_conjunct2(259)), 0), pred(comma_conjunct1(comma_conjunct2(259)), 0)))), pred(comma_conjunct1(259), 0))')).
% 130.12/126.01 cnf(10, plain, [-(vd1123 = vd1129)], clausify('holds(258, 1150, 0)')).
% 130.12/126.01 cnf(11, plain, [-(vd1129 = vd1130)], clausify('and(and(and(and(holds(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(242)))))), 1133, 0), and(holds(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(242)))))), 1132, 0), and(holds(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(242))))), 1131, 0), and(pred(conjunct1(conjunct2(conjunct2(conjunct2(242)))), 2), pred(conjunct1(conjunct2(conjunct2(conjunct2(242)))), 1))))), and(pred(conjunct1(conjunct2(conjunct2(242))), 2), pred(conjunct1(conjunct2(conjunct2(242))), 1))), and(pred(conjunct1(conjunct2(242)), 2), pred(conjunct1(conjunct2(242)), 1))), and(pred(conjunct1(242), 2), pred(conjunct1(242), 1)))')).
% 130.12/126.01 cnf(12, plain, [-(rpoint(vd1130))], clausify('and(and(and(and(holds(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(242)))))), 1133, 0), and(holds(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(242)))))), 1132, 0), and(holds(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(242))))), 1131, 0), and(pred(conjunct1(conjunct2(conjunct2(conjunct2(242)))), 2), pred(conjunct1(conjunct2(conjunct2(conjunct2(242)))), 1))))), and(pred(conjunct1(conjunct2(conjunct2(242))), 2), pred(conjunct1(conjunct2(conjunct2(242))), 1))), and(pred(conjunct1(conjunct2(242)), 2), pred(conjunct1(conjunct2(242)), 1))), and(pred(conjunct1(242), 2), pred(conjunct1(242), 1)))')).
% 130.12/126.01 cnf(13, plain, [-(vd1125 = vd1126)], clausify('and(and(and(and(holds(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(242)))))), 1133, 0), and(holds(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(242)))))), 1132, 0), and(holds(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(242))))), 1131, 0), and(pred(conjunct1(conjunct2(conjunct2(conjunct2(242)))), 2), pred(conjunct1(conjunct2(conjunct2(conjunct2(242)))), 1))))), and(pred(conjunct1(conjunct2(conjunct2(242))), 2), pred(conjunct1(conjunct2(conjunct2(242))), 1))), and(pred(conjunct1(conjunct2(242)), 2), pred(conjunct1(conjunct2(242)), 1))), and(pred(conjunct1(242), 2), pred(conjunct1(242), 1)))')).
% 130.12/126.01 cnf(14, plain, [-(rpoint(vd1126))], clausify('and(and(and(and(holds(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(242)))))), 1133, 0), and(holds(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(conjunct2(242)))))), 1132, 0), and(holds(conjunct1(conjunct2(conjunct2(conjunct2(conjunct2(242))))), 1131, 0), and(pred(conjunct1(conjunct2(conjunct2(conjunct2(242)))), 2), pred(conjunct1(conjunct2(conjunct2(conjunct2(242)))), 1))))), and(pred(conjunct1(conjunct2(conjunct2(242))), 2), pred(conjunct1(conjunct2(conjunct2(242))), 1))), and(pred(conjunct1(conjunct2(242)), 2), pred(conjunct1(conjunct2(242)), 1))), and(pred(conjunct1(242), 2), pred(conjunct1(242), 1)))')).
% 130.12/126.01 cnf(15, plain, [-(rline(vd1151))], clausify('pred(259, 0)')).
% 130.12/126.01 cnf(16, plain, [-(rR(4 ^ [_15729, _15728, _15727, _15726, _15725, _15724, _15723, _15722], _15726, _15728)), ron(_15728, _15724), -(ron(_15728, _15722)), -(rinside(_15728, _15722)), _15728 = _15729, rpoint(_15729), ron(_15726, _15724), rinside(_15726, _15722), _15726 = _15727, rpoint(_15727), _15724 = _15725, rline(_15725), _15722 = _15723, rcircle(_15723)], clausify('qu(cond(axiom(61), 0), imp(cond(axiom(61), 0)))')).
% 130.12/126.01 cnf(17, plain, [-(ron(4 ^ [_15729, _15728, _15727, _15726, _15725, _15724, _15723, _15722], _15722)), ron(_15728, _15724), -(ron(_15728, _15722)), -(rinside(_15728, _15722)), _15728 = _15729, rpoint(_15729), ron(_15726, _15724), rinside(_15726, _15722), _15726 = _15727, rpoint(_15727), _15724 = _15725, rline(_15725), _15722 = _15723, rcircle(_15723)], clausify('qu(cond(axiom(61), 0), imp(cond(axiom(61), 0)))')).
% 130.12/126.01 cnf(18, plain, [-(ron(4 ^ [_15729, _15728, _15727, _15726, _15725, _15724, _15723, _15722], _15724)), ron(_15728, _15724), -(ron(_15728, _15722)), -(rinside(_15728, _15722)), _15728 = _15729, rpoint(_15729), ron(_15726, _15724), rinside(_15726, _15722), _15726 = _15727, rpoint(_15727), _15724 = _15725, rline(_15725), _15722 = _15723, rcircle(_15723)], clausify('qu(cond(axiom(61), 0), imp(cond(axiom(61), 0)))')).
% 130.12/126.01 cnf(19, plain, [-(rpoint(4 ^ [_15729, _15728, _15727, _15726, _15725, _15724, _15723, _15722])), ron(_15728, _15724), -(ron(_15728, _15722)), -(rinside(_15728, _15722)), _15728 = _15729, rpoint(_15729), ron(_15726, _15724), rinside(_15726, _15722), _15726 = _15727, rpoint(_15727), _15724 = _15725, rline(_15725), _15722 = _15723, rcircle(_15723)], clausify('qu(cond(axiom(61), 0), imp(cond(axiom(61), 0)))')).
% 130.12/126.01 cnf(20, plain, [rcenter(_17815, _17816), -(rinside(_17815, _17816))], clausify('qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))')).
% 130.12/126.01
% 130.12/126.01 cnf('1',plain,[rR(4 ^ [vd1126, vd1125, vd1130, vd1123, vd1151, vd1151, vd1152, vd1152], vd1123, vd1125), ron(4 ^ [vd1126, vd1125, vd1130, vd1123, vd1151, vd1151, vd1152, vd1152], vd1152), ron(4 ^ [vd1126, vd1125, vd1130, vd1123, vd1151, vd1151, vd1152, vd1152], vd1151), rpoint(4 ^ [vd1126, vd1125, vd1130, vd1123, vd1151, vd1151, vd1152, vd1152])],start(1,bind([[_19910], [4 ^ [vd1126, vd1125, vd1130, vd1123, vd1151, vd1151, vd1152, vd1152]]]))).
% 130.12/126.01 cnf('1.1',plain,[-(rR(4 ^ [vd1126, vd1125, vd1130, vd1123, vd1151, vd1151, vd1152, vd1152], vd1123, vd1125)), ron(vd1125, vd1151), -(ron(vd1125, vd1152)), -(rinside(vd1125, vd1152)), vd1125 = vd1126, rpoint(vd1126), ron(vd1123, vd1151), rinside(vd1123, vd1152), vd1123 = vd1130, rpoint(vd1130), vd1151 = vd1151, rline(vd1151), vd1152 = vd1152, rcircle(vd1152)],extension(16,bind([[_15728, _15729, _15726, _15727, _15724, _15725, _15722, _15723], [vd1125, vd1126, vd1123, vd1130, vd1151, vd1151, vd1152, vd1152]]))).
% 130.12/126.01 cnf('1.1.1',plain,[-(ron(vd1125, vd1151))],extension(8)).
% 130.12/126.01 cnf('1.1.2',plain,[ron(vd1125, vd1152)],extension(4)).
% 130.12/126.01 cnf('1.1.3',plain,[rinside(vd1125, vd1152)],extension(5)).
% 130.12/126.01 cnf('1.1.4',plain,[-(vd1125 = vd1126)],extension(13)).
% 130.12/126.01 cnf('1.1.5',plain,[-(rpoint(vd1126))],extension(14)).
% 130.12/126.01 cnf('1.1.6',plain,[-(ron(vd1123, vd1151))],extension(9)).
% 130.12/126.01 cnf('1.1.7',plain,[-(rinside(vd1123, vd1152)), rcenter(vd1123, vd1152)],extension(20,bind([[_17815, _17816], [vd1123, vd1152]]))).
% 130.12/126.01 cnf('1.1.7.1',plain,[-(rcenter(vd1123, vd1152))],extension(6)).
% 130.12/126.01 cnf('1.1.8',plain,[-(vd1123 = vd1130), vd1123 = vd1129, vd1129 = vd1130],extension(3,bind([[_14943, _14944, _14945], [vd1123, vd1129, vd1130]]))).
% 130.12/126.01 cnf('1.1.8.1',plain,[-(vd1123 = vd1129)],extension(10)).
% 130.12/126.01 cnf('1.1.8.2',plain,[-(vd1129 = vd1130)],extension(11)).
% 130.12/126.01 cnf('1.1.9',plain,[-(rpoint(vd1130))],extension(12)).
% 130.12/126.01 cnf('1.1.10',plain,[-(vd1151 = vd1151)],extension(2,bind([[_14927], [vd1151]]))).
% 130.12/126.01 cnf('1.1.11',plain,[-(rline(vd1151))],extension(15)).
% 130.12/126.01 cnf('1.1.12',plain,[-(vd1152 = vd1152)],extension(2,bind([[_14927], [vd1152]]))).
% 130.12/126.01 cnf('1.1.13',plain,[-(rcircle(vd1152))],extension(7)).
% 130.12/126.01 cnf('1.2',plain,[-(ron(4 ^ [vd1126, vd1125, vd1130, vd1123, vd1151, vd1151, vd1152, vd1152], vd1152)), ron(vd1125, vd1151), -(ron(vd1125, vd1152)), -(rinside(vd1125, vd1152)), vd1125 = vd1126, rpoint(vd1126), ron(vd1123, vd1151), rinside(vd1123, vd1152), vd1123 = vd1130, rpoint(vd1130), vd1151 = vd1151, rline(vd1151), vd1152 = vd1152, rcircle(vd1152)],extension(17,bind([[_15728, _15729, _15726, _15727, _15724, _15725, _15722, _15723], [vd1125, vd1126, vd1123, vd1130, vd1151, vd1151, vd1152, vd1152]]))).
% 130.12/126.01 cnf('1.2.1',plain,[-(ron(vd1125, vd1151))],extension(8)).
% 130.12/126.01 cnf('1.2.2',plain,[ron(vd1125, vd1152)],extension(4)).
% 130.12/126.01 cnf('1.2.3',plain,[rinside(vd1125, vd1152)],extension(5)).
% 130.12/126.01 cnf('1.2.4',plain,[-(vd1125 = vd1126)],extension(13)).
% 130.12/126.01 cnf('1.2.5',plain,[-(rpoint(vd1126))],extension(14)).
% 130.12/126.01 cnf('1.2.6',plain,[-(ron(vd1123, vd1151))],extension(9)).
% 130.12/126.01 cnf('1.2.7',plain,[-(rinside(vd1123, vd1152)), rcenter(vd1123, vd1152)],extension(20,bind([[_17815, _17816], [vd1123, vd1152]]))).
% 130.12/126.01 cnf('1.2.7.1',plain,[-(rcenter(vd1123, vd1152))],extension(6)).
% 130.12/126.01 cnf('1.2.8',plain,[-(vd1123 = vd1130), vd1123 = vd1129, vd1129 = vd1130],extension(3,bind([[_14943, _14944, _14945], [vd1123, vd1129, vd1130]]))).
% 130.12/126.01 cnf('1.2.8.1',plain,[-(vd1123 = vd1129)],extension(10)).
% 130.12/126.01 cnf('1.2.8.2',plain,[-(vd1129 = vd1130)],extension(11)).
% 130.12/126.01 cnf('1.2.9',plain,[-(rpoint(vd1130))],extension(12)).
% 130.12/126.01 cnf('1.2.10',plain,[-(vd1151 = vd1151)],extension(2,bind([[_14927], [vd1151]]))).
% 130.12/126.01 cnf('1.2.11',plain,[-(rline(vd1151))],extension(15)).
% 130.12/126.01 cnf('1.2.12',plain,[-(vd1152 = vd1152)],extension(2,bind([[_14927], [vd1152]]))).
% 130.12/126.01 cnf('1.2.13',plain,[-(rcircle(vd1152))],extension(7)).
% 130.12/126.01 cnf('1.3',plain,[-(ron(4 ^ [vd1126, vd1125, vd1130, vd1123, vd1151, vd1151, vd1152, vd1152], vd1151)), ron(vd1125, vd1151), -(ron(vd1125, vd1152)), -(rinside(vd1125, vd1152)), vd1125 = vd1126, rpoint(vd1126), ron(vd1123, vd1151), rinside(vd1123, vd1152), vd1123 = vd1130, rpoint(vd1130), vd1151 = vd1151, rline(vd1151), vd1152 = vd1152, rcircle(vd1152)],extension(18,bind([[_15728, _15729, _15726, _15727, _15724, _15725, _15722, _15723], [vd1125, vd1126, vd1123, vd1130, vd1151, vd1151, vd1152, vd1152]]))).
% 130.12/126.01 cnf('1.3.1',plain,[-(ron(vd1125, vd1151))],extension(8)).
% 130.12/126.01 cnf('1.3.2',plain,[ron(vd1125, vd1152)],extension(4)).
% 130.12/126.01 cnf('1.3.3',plain,[rinside(vd1125, vd1152)],extension(5)).
% 130.12/126.01 cnf('1.3.4',plain,[-(vd1125 = vd1126)],extension(13)).
% 130.12/126.01 cnf('1.3.5',plain,[-(rpoint(vd1126))],extension(14)).
% 130.12/126.01 cnf('1.3.6',plain,[-(ron(vd1123, vd1151))],extension(9)).
% 130.12/126.01 cnf('1.3.7',plain,[-(rinside(vd1123, vd1152)), rcenter(vd1123, vd1152)],extension(20,bind([[_17815, _17816], [vd1123, vd1152]]))).
% 130.12/126.01 cnf('1.3.7.1',plain,[-(rcenter(vd1123, vd1152))],extension(6)).
% 130.12/126.01 cnf('1.3.8',plain,[-(vd1123 = vd1130), vd1123 = vd1129, vd1129 = vd1130],extension(3,bind([[_14943, _14944, _14945], [vd1123, vd1129, vd1130]]))).
% 130.12/126.01 cnf('1.3.8.1',plain,[-(vd1123 = vd1129)],extension(10)).
% 130.12/126.01 cnf('1.3.8.2',plain,[-(vd1129 = vd1130)],extension(11)).
% 130.12/126.01 cnf('1.3.9',plain,[-(rpoint(vd1130))],extension(12)).
% 130.12/126.01 cnf('1.3.10',plain,[-(vd1151 = vd1151)],extension(2,bind([[_14927], [vd1151]]))).
% 130.12/126.01 cnf('1.3.11',plain,[-(rline(vd1151))],extension(15)).
% 130.12/126.01 cnf('1.3.12',plain,[-(vd1152 = vd1152)],extension(2,bind([[_14927], [vd1152]]))).
% 130.12/126.01 cnf('1.3.13',plain,[-(rcircle(vd1152))],extension(7)).
% 130.12/126.01 cnf('1.4',plain,[-(rpoint(4 ^ [vd1126, vd1125, vd1130, vd1123, vd1151, vd1151, vd1152, vd1152])), ron(vd1125, vd1151), -(ron(vd1125, vd1152)), -(rinside(vd1125, vd1152)), vd1125 = vd1126, rpoint(vd1126), ron(vd1123, vd1151), rinside(vd1123, vd1152), vd1123 = vd1130, rpoint(vd1130), vd1151 = vd1151, rline(vd1151), vd1152 = vd1152, rcircle(vd1152)],extension(19,bind([[_15728, _15729, _15726, _15727, _15724, _15725, _15722, _15723], [vd1125, vd1126, vd1123, vd1130, vd1151, vd1151, vd1152, vd1152]]))).
% 130.12/126.01 cnf('1.4.1',plain,[-(ron(vd1125, vd1151))],extension(8)).
% 130.12/126.01 cnf('1.4.2',plain,[ron(vd1125, vd1152)],extension(4)).
% 130.12/126.01 cnf('1.4.3',plain,[rinside(vd1125, vd1152)],extension(5)).
% 130.12/126.01 cnf('1.4.4',plain,[-(vd1125 = vd1126)],extension(13)).
% 130.12/126.01 cnf('1.4.5',plain,[-(rpoint(vd1126))],extension(14)).
% 130.12/126.01 cnf('1.4.6',plain,[-(ron(vd1123, vd1151))],extension(9)).
% 130.12/126.01 cnf('1.4.7',plain,[-(rinside(vd1123, vd1152)), rcenter(vd1123, vd1152)],extension(20,bind([[_17815, _17816], [vd1123, vd1152]]))).
% 130.12/126.01 cnf('1.4.7.1',plain,[-(rcenter(vd1123, vd1152))],extension(6)).
% 130.12/126.01 cnf('1.4.8',plain,[-(vd1123 = vd1130), vd1123 = vd1129, vd1129 = vd1130],extension(3,bind([[_14943, _14944, _14945], [vd1123, vd1129, vd1130]]))).
% 130.12/126.01 cnf('1.4.8.1',plain,[-(vd1123 = vd1129)],extension(10)).
% 130.12/126.01 cnf('1.4.8.2',plain,[-(vd1129 = vd1130)],extension(11)).
% 130.12/126.01 cnf('1.4.9',plain,[-(rpoint(vd1130))],extension(12)).
% 130.12/126.01 cnf('1.4.10',plain,[-(vd1151 = vd1151)],extension(2,bind([[_14927], [vd1151]]))).
% 130.12/126.01 cnf('1.4.11',plain,[-(rline(vd1151))],extension(15)).
% 130.12/126.01 cnf('1.4.12',plain,[-(vd1152 = vd1152)],extension(2,bind([[_14927], [vd1152]]))).
% 130.12/126.01 cnf('1.4.13',plain,[-(rcircle(vd1152))],extension(7)).
% 130.12/126.01 %-----------------------------------------------------
% 130.22/126.02
% 130.22/126.02 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------