%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : GEO281+1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n010.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:23 EDT 2022
% Result : Theorem 120.07s 115.68s
% Output : Proof 120.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GEO281+1 : TPTP v8.1.0. Released v4.1.0.
% 0.13/0.14 % Command : leancop_casc.sh %s %d
% 0.13/0.35 % Computer : n010.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Sat Jun 18 02:34:53 EDT 2022
% 0.20/0.36 % CPUTime :
% 120.07/115.68 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 120.07/115.69 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 120.07/115.69
% 120.07/115.69 %-----------------------------------------------------
% 120.07/115.69 fof('qe(248)', conjecture, ? [_140616] : (rR(_140616, vd1123, vd1125) & ron(_140616, vd1139) & ron(_140616, vd1138) & rpoint(_140616)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'qe(248)')).
% 120.07/115.69 fof('neg(neg(comma_conjunct2(247)))', axiom, ~ ron(vd1125, vd1139), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'neg(neg(comma_conjunct2(247)))')).
% 120.07/115.69 fof('neg(neg(247))', axiom, ~ rinside(vd1125, vd1139), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'neg(neg(247))')).
% 120.07/115.69 fof('and(and(pred(comma_conjunct2(comma_conjunct2(comma_conjunct2(246))), 0), and(pred(comma_conjunct1(comma_conjunct2(comma_conjunct2(246))), 0), and(pred(comma_conjunct2(comma_conjunct2(246)), 0), pred(comma_conjunct1(comma_conjunct2(246)), 0)))), pred(comma_conjunct1(246), 0))', axiom, ron(vd1136, vd1139) & rcenter(vd1123, vd1139) & rcircle(vd1139) & ron(vd1125, vd1138) & ron(vd1123, vd1138), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'and(and(pred(comma_conjunct2(comma_conjunct2(comma_conjunct2(246))), 0), and(pred(comma_conjunct1(comma_conjunct2(comma_conjunct2(246))), 0), and(pred(comma_conjunct2(comma_conjunct2(246)), 0), pred(comma_conjunct1(comma_conjunct2(246)), 0)))), pred(comma_conjunct1(246), 0))')).
% 120.07/115.69 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/sandbox2/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)))')).
% 120.07/115.69 fof('pred(246, 0)', axiom, rline(vd1138), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'pred(246, 0)')).
% 120.07/115.69 fof('qu(cond(axiom(61), 0), imp(cond(axiom(61), 0)))', axiom, ! [_141302, _141305, _141308, _141311, _141314, _141317, _141320, _141323] : (ron(_141320, _141308) & ~ ron(_141320, _141302) & ~ rinside(_141320, _141302) & _141320 = _141323 & rpoint(_141323) & ron(_141314, _141308) & rinside(_141314, _141302) & _141314 = _141317 & rpoint(_141317) & _141308 = _141311 & rline(_141311) & _141302 = _141305 & rcircle(_141305) => ? [_141437] : (rR(_141437, _141314, _141320) & ron(_141437, _141302) & ron(_141437, _141308) & rpoint(_141437))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'qu(cond(axiom(61), 0), imp(cond(axiom(61), 0)))')).
% 120.07/115.69 fof('qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))', axiom, ! [_142055, _142058] : (rcenter(_142055, _142058) => rinside(_142055, _142058)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', 'qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))')).
% 120.07/115.69
% 120.07/115.69 cnf(1, plain, [rR(_19137, vd1123, vd1125), ron(_19137, vd1139), ron(_19137, vd1138), rpoint(_19137)], clausify('qe(248)')).
% 120.07/115.69 cnf(2, plain, [-(_14399 = _14399)], theory(equality)).
% 120.07/115.69 cnf(3, plain, [ron(vd1125, vd1139)], clausify('neg(neg(comma_conjunct2(247)))')).
% 120.07/115.69 cnf(4, plain, [rinside(vd1125, vd1139)], clausify('neg(neg(247))')).
% 120.07/115.69 cnf(5, plain, [-(rcenter(vd1123, vd1139))], clausify('and(and(pred(comma_conjunct2(comma_conjunct2(comma_conjunct2(246))), 0), and(pred(comma_conjunct1(comma_conjunct2(comma_conjunct2(246))), 0), and(pred(comma_conjunct2(comma_conjunct2(246)), 0), pred(comma_conjunct1(comma_conjunct2(246)), 0)))), pred(comma_conjunct1(246), 0))')).
% 120.07/115.69 cnf(6, plain, [-(rcircle(vd1139))], clausify('and(and(pred(comma_conjunct2(comma_conjunct2(comma_conjunct2(246))), 0), and(pred(comma_conjunct1(comma_conjunct2(comma_conjunct2(246))), 0), and(pred(comma_conjunct2(comma_conjunct2(246)), 0), pred(comma_conjunct1(comma_conjunct2(246)), 0)))), pred(comma_conjunct1(246), 0))')).
% 120.07/115.69 cnf(7, plain, [-(ron(vd1125, vd1138))], clausify('and(and(pred(comma_conjunct2(comma_conjunct2(comma_conjunct2(246))), 0), and(pred(comma_conjunct1(comma_conjunct2(comma_conjunct2(246))), 0), and(pred(comma_conjunct2(comma_conjunct2(246)), 0), pred(comma_conjunct1(comma_conjunct2(246)), 0)))), pred(comma_conjunct1(246), 0))')).
% 120.07/115.69 cnf(8, plain, [-(ron(vd1123, vd1138))], clausify('and(and(pred(comma_conjunct2(comma_conjunct2(comma_conjunct2(246))), 0), and(pred(comma_conjunct1(comma_conjunct2(comma_conjunct2(246))), 0), and(pred(comma_conjunct2(comma_conjunct2(246)), 0), pred(comma_conjunct1(comma_conjunct2(246)), 0)))), pred(comma_conjunct1(246), 0))')).
% 120.07/115.69 cnf(9, 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)))')).
% 120.07/115.69 cnf(10, 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)))')).
% 120.07/115.69 cnf(11, plain, [-(vd1123 = vd1124)], 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)))')).
% 120.07/115.69 cnf(12, plain, [-(rpoint(vd1124))], 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)))')).
% 120.07/115.69 cnf(13, plain, [-(rline(vd1138))], clausify('pred(246, 0)')).
% 120.07/115.69 cnf(14, plain, [-(rR(2 ^ [_15083, _15082, _15081, _15080, _15079, _15078, _15077, _15076], _15080, _15082)), ron(_15082, _15078), -(ron(_15082, _15076)), -(rinside(_15082, _15076)), _15082 = _15083, rpoint(_15083), ron(_15080, _15078), rinside(_15080, _15076), _15080 = _15081, rpoint(_15081), _15078 = _15079, rline(_15079), _15076 = _15077, rcircle(_15077)], clausify('qu(cond(axiom(61), 0), imp(cond(axiom(61), 0)))')).
% 120.07/115.69 cnf(15, plain, [-(ron(2 ^ [_15083, _15082, _15081, _15080, _15079, _15078, _15077, _15076], _15076)), ron(_15082, _15078), -(ron(_15082, _15076)), -(rinside(_15082, _15076)), _15082 = _15083, rpoint(_15083), ron(_15080, _15078), rinside(_15080, _15076), _15080 = _15081, rpoint(_15081), _15078 = _15079, rline(_15079), _15076 = _15077, rcircle(_15077)], clausify('qu(cond(axiom(61), 0), imp(cond(axiom(61), 0)))')).
% 120.07/115.69 cnf(16, plain, [-(ron(2 ^ [_15083, _15082, _15081, _15080, _15079, _15078, _15077, _15076], _15078)), ron(_15082, _15078), -(ron(_15082, _15076)), -(rinside(_15082, _15076)), _15082 = _15083, rpoint(_15083), ron(_15080, _15078), rinside(_15080, _15076), _15080 = _15081, rpoint(_15081), _15078 = _15079, rline(_15079), _15076 = _15077, rcircle(_15077)], clausify('qu(cond(axiom(61), 0), imp(cond(axiom(61), 0)))')).
% 120.07/115.69 cnf(17, plain, [-(rpoint(2 ^ [_15083, _15082, _15081, _15080, _15079, _15078, _15077, _15076])), ron(_15082, _15078), -(ron(_15082, _15076)), -(rinside(_15082, _15076)), _15082 = _15083, rpoint(_15083), ron(_15080, _15078), rinside(_15080, _15076), _15080 = _15081, rpoint(_15081), _15078 = _15079, rline(_15079), _15076 = _15077, rcircle(_15077)], clausify('qu(cond(axiom(61), 0), imp(cond(axiom(61), 0)))')).
% 120.07/115.69 cnf(18, plain, [rcenter(_17254, _17255), -(rinside(_17254, _17255))], clausify('qu(cond(axiom(77), 0), imp(cond(axiom(77), 0)))')).
% 120.07/115.69
% 120.07/115.69 cnf('1',plain,[rR(2 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139], vd1123, vd1125), ron(2 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139], vd1139), ron(2 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139], vd1138), rpoint(2 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139])],start(1,bind([[_19137], [2 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139]]]))).
% 120.07/115.69 cnf('1.1',plain,[-(rR(2 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139], vd1123, vd1125)), ron(vd1125, vd1138), -(ron(vd1125, vd1139)), -(rinside(vd1125, vd1139)), vd1125 = vd1126, rpoint(vd1126), ron(vd1123, vd1138), rinside(vd1123, vd1139), vd1123 = vd1124, rpoint(vd1124), vd1138 = vd1138, rline(vd1138), vd1139 = vd1139, rcircle(vd1139)],extension(14,bind([[_15082, _15083, _15080, _15081, _15078, _15079, _15076, _15077], [vd1125, vd1126, vd1123, vd1124, vd1138, vd1138, vd1139, vd1139]]))).
% 120.07/115.69 cnf('1.1.1',plain,[-(ron(vd1125, vd1138))],extension(7)).
% 120.07/115.69 cnf('1.1.2',plain,[ron(vd1125, vd1139)],extension(3)).
% 120.07/115.69 cnf('1.1.3',plain,[rinside(vd1125, vd1139)],extension(4)).
% 120.07/115.69 cnf('1.1.4',plain,[-(vd1125 = vd1126)],extension(9)).
% 120.07/115.69 cnf('1.1.5',plain,[-(rpoint(vd1126))],extension(10)).
% 120.07/115.69 cnf('1.1.6',plain,[-(ron(vd1123, vd1138))],extension(8)).
% 120.07/115.69 cnf('1.1.7',plain,[-(rinside(vd1123, vd1139)), rcenter(vd1123, vd1139)],extension(18,bind([[_17254, _17255], [vd1123, vd1139]]))).
% 120.07/115.69 cnf('1.1.7.1',plain,[-(rcenter(vd1123, vd1139))],extension(5)).
% 120.07/115.69 cnf('1.1.8',plain,[-(vd1123 = vd1124)],extension(11)).
% 120.07/115.69 cnf('1.1.9',plain,[-(rpoint(vd1124))],extension(12)).
% 120.07/115.69 cnf('1.1.10',plain,[-(vd1138 = vd1138)],extension(2,bind([[_14399], [vd1138]]))).
% 120.07/115.69 cnf('1.1.11',plain,[-(rline(vd1138))],extension(13)).
% 120.07/115.69 cnf('1.1.12',plain,[-(vd1139 = vd1139)],extension(2,bind([[_14399], [vd1139]]))).
% 120.07/115.69 cnf('1.1.13',plain,[-(rcircle(vd1139))],extension(6)).
% 120.07/115.69 cnf('1.2',plain,[-(ron(2 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139], vd1139)), ron(vd1125, vd1138), -(ron(vd1125, vd1139)), -(rinside(vd1125, vd1139)), vd1125 = vd1126, rpoint(vd1126), ron(vd1123, vd1138), rinside(vd1123, vd1139), vd1123 = vd1124, rpoint(vd1124), vd1138 = vd1138, rline(vd1138), vd1139 = vd1139, rcircle(vd1139)],extension(15,bind([[_15082, _15083, _15080, _15081, _15078, _15079, _15076, _15077], [vd1125, vd1126, vd1123, vd1124, vd1138, vd1138, vd1139, vd1139]]))).
% 120.07/115.69 cnf('1.2.1',plain,[-(ron(vd1125, vd1138))],extension(7)).
% 120.07/115.69 cnf('1.2.2',plain,[ron(vd1125, vd1139)],extension(3)).
% 120.07/115.69 cnf('1.2.3',plain,[rinside(vd1125, vd1139)],extension(4)).
% 120.07/115.69 cnf('1.2.4',plain,[-(vd1125 = vd1126)],extension(9)).
% 120.07/115.69 cnf('1.2.5',plain,[-(rpoint(vd1126))],extension(10)).
% 120.07/115.69 cnf('1.2.6',plain,[-(ron(vd1123, vd1138))],extension(8)).
% 120.07/115.69 cnf('1.2.7',plain,[-(rinside(vd1123, vd1139)), rcenter(vd1123, vd1139)],extension(18,bind([[_17254, _17255], [vd1123, vd1139]]))).
% 120.07/115.69 cnf('1.2.7.1',plain,[-(rcenter(vd1123, vd1139))],extension(5)).
% 120.07/115.69 cnf('1.2.8',plain,[-(vd1123 = vd1124)],extension(11)).
% 120.07/115.69 cnf('1.2.9',plain,[-(rpoint(vd1124))],extension(12)).
% 120.07/115.69 cnf('1.2.10',plain,[-(vd1138 = vd1138)],extension(2,bind([[_14399], [vd1138]]))).
% 120.07/115.69 cnf('1.2.11',plain,[-(rline(vd1138))],extension(13)).
% 120.07/115.69 cnf('1.2.12',plain,[-(vd1139 = vd1139)],extension(2,bind([[_14399], [vd1139]]))).
% 120.07/115.69 cnf('1.2.13',plain,[-(rcircle(vd1139))],extension(6)).
% 120.07/115.69 cnf('1.3',plain,[-(ron(2 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139], vd1138)), ron(vd1125, vd1138), -(ron(vd1125, vd1139)), -(rinside(vd1125, vd1139)), vd1125 = vd1126, rpoint(vd1126), ron(vd1123, vd1138), rinside(vd1123, vd1139), vd1123 = vd1124, rpoint(vd1124), vd1138 = vd1138, rline(vd1138), vd1139 = vd1139, rcircle(vd1139)],extension(16,bind([[_15082, _15083, _15080, _15081, _15078, _15079, _15076, _15077], [vd1125, vd1126, vd1123, vd1124, vd1138, vd1138, vd1139, vd1139]]))).
% 120.07/115.69 cnf('1.3.1',plain,[-(ron(vd1125, vd1138))],extension(7)).
% 120.07/115.69 cnf('1.3.2',plain,[ron(vd1125, vd1139)],extension(3)).
% 120.07/115.69 cnf('1.3.3',plain,[rinside(vd1125, vd1139)],extension(4)).
% 120.07/115.69 cnf('1.3.4',plain,[-(vd1125 = vd1126)],extension(9)).
% 120.07/115.69 cnf('1.3.5',plain,[-(rpoint(vd1126))],extension(10)).
% 120.07/115.69 cnf('1.3.6',plain,[-(ron(vd1123, vd1138))],extension(8)).
% 120.07/115.69 cnf('1.3.7',plain,[-(rinside(vd1123, vd1139)), rcenter(vd1123, vd1139)],extension(18,bind([[_17254, _17255], [vd1123, vd1139]]))).
% 120.07/115.69 cnf('1.3.7.1',plain,[-(rcenter(vd1123, vd1139))],extension(5)).
% 120.07/115.69 cnf('1.3.8',plain,[-(vd1123 = vd1124)],extension(11)).
% 120.07/115.69 cnf('1.3.9',plain,[-(rpoint(vd1124))],extension(12)).
% 120.07/115.69 cnf('1.3.10',plain,[-(vd1138 = vd1138)],extension(2,bind([[_14399], [vd1138]]))).
% 120.07/115.69 cnf('1.3.11',plain,[-(rline(vd1138))],extension(13)).
% 120.07/115.69 cnf('1.3.12',plain,[-(vd1139 = vd1139)],extension(2,bind([[_14399], [vd1139]]))).
% 120.07/115.69 cnf('1.3.13',plain,[-(rcircle(vd1139))],extension(6)).
% 120.07/115.69 cnf('1.4',plain,[-(rpoint(2 ^ [vd1126, vd1125, vd1124, vd1123, vd1138, vd1138, vd1139, vd1139])), ron(vd1125, vd1138), -(ron(vd1125, vd1139)), -(rinside(vd1125, vd1139)), vd1125 = vd1126, rpoint(vd1126), ron(vd1123, vd1138), rinside(vd1123, vd1139), vd1123 = vd1124, rpoint(vd1124), vd1138 = vd1138, rline(vd1138), vd1139 = vd1139, rcircle(vd1139)],extension(17,bind([[_15082, _15083, _15080, _15081, _15078, _15079, _15076, _15077], [vd1125, vd1126, vd1123, vd1124, vd1138, vd1138, vd1139, vd1139]]))).
% 120.07/115.69 cnf('1.4.1',plain,[-(ron(vd1125, vd1138))],extension(7)).
% 120.07/115.69 cnf('1.4.2',plain,[ron(vd1125, vd1139)],extension(3)).
% 120.07/115.69 cnf('1.4.3',plain,[rinside(vd1125, vd1139)],extension(4)).
% 120.07/115.69 cnf('1.4.4',plain,[-(vd1125 = vd1126)],extension(9)).
% 120.07/115.69 cnf('1.4.5',plain,[-(rpoint(vd1126))],extension(10)).
% 120.07/115.69 cnf('1.4.6',plain,[-(ron(vd1123, vd1138))],extension(8)).
% 120.07/115.69 cnf('1.4.7',plain,[-(rinside(vd1123, vd1139)), rcenter(vd1123, vd1139)],extension(18,bind([[_17254, _17255], [vd1123, vd1139]]))).
% 120.07/115.69 cnf('1.4.7.1',plain,[-(rcenter(vd1123, vd1139))],extension(5)).
% 120.07/115.69 cnf('1.4.8',plain,[-(vd1123 = vd1124)],extension(11)).
% 120.07/115.69 cnf('1.4.9',plain,[-(rpoint(vd1124))],extension(12)).
% 120.07/115.69 cnf('1.4.10',plain,[-(vd1138 = vd1138)],extension(2,bind([[_14399], [vd1138]]))).
% 120.07/115.69 cnf('1.4.11',plain,[-(rline(vd1138))],extension(13)).
% 120.07/115.69 cnf('1.4.12',plain,[-(vd1139 = vd1139)],extension(2,bind([[_14399], [vd1139]]))).
% 120.07/115.69 cnf('1.4.13',plain,[-(rcircle(vd1139))],extension(6)).
% 120.07/115.69 %-----------------------------------------------------
% 120.09/115.70
% 120.09/115.70 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------