%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : GEO013-3 : TPTP v8.1.0. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n012.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 06:21:34 EDT 2022
% Result : Unsatisfiable 4.09s 4.29s
% Output : Refutation 4.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 13
% Syntax : Number of clauses : 37 ( 21 unt; 7 nHn; 37 RR)
% Number of literals : 63 ( 0 equ; 25 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(64,axiom,
( ~ between(u,v,w)
| colinear(w,v,u) ),
file('GEO013-3.p',unknown),
[] ).
cnf(65,axiom,
( ~ between(u,v,w)
| colinear(u,w,v) ),
file('GEO013-3.p',unknown),
[] ).
cnf(66,axiom,
( ~ between(u,v,w)
| colinear(v,u,w) ),
file('GEO013-3.p',unknown),
[] ).
cnf(68,axiom,
( ~ colinear(u,v,w)
| colinear(v,w,u) ),
file('GEO013-3.p',unknown),
[] ).
cnf(70,axiom,
( ~ colinear(u,v,w)
| colinear(w,u,v) ),
file('GEO013-3.p',unknown),
[] ).
cnf(78,axiom,
( ~ colinear(u,v,w)
| ~ colinear(u,v,x)
| equal(u,v)
| colinear(u,x,w) ),
file('GEO013-3.p',unknown),
[] ).
cnf(81,axiom,
( ~ colinear(u,v,w)
| ~ colinear(x,v,w)
| equal(w,v)
| colinear(u,x,v) ),
file('GEO013-3.p',unknown),
[] ).
cnf(82,axiom,
~ equal(b,a),
file('GEO013-3.p',unknown),
[] ).
cnf(83,axiom,
colinear(a,b,d1),
file('GEO013-3.p',unknown),
[] ).
cnf(84,axiom,
colinear(a,b,d2),
file('GEO013-3.p',unknown),
[] ).
cnf(85,axiom,
colinear(a,b,d3),
file('GEO013-3.p',unknown),
[] ).
cnf(86,axiom,
~ colinear(d1,d2,d3),
file('GEO013-3.p',unknown),
[] ).
cnf(108,axiom,
( ~ colinear(u,v,w)
| between(w,u,v)
| between(v,w,u)
| between(u,v,w) ),
file('GEO013-3.p',unknown),
[] ).
cnf(114,plain,
~ between(d1,d3,d2),
inference(res,[status(thm),theory(equality)],[65,86]),
[iquote('0:Res:65.1,86.0')] ).
cnf(117,plain,
( ~ colinear(d1,u,d3)
| ~ colinear(d1,u,d2)
| equal(d1,u) ),
inference(res,[status(thm),theory(equality)],[78,86]),
[iquote('0:Res:78.2,86.0')] ).
cnf(120,plain,
~ between(d3,d2,d1),
inference(res,[status(thm),theory(equality)],[64,86]),
[iquote('0:Res:64.1,86.0')] ).
cnf(125,plain,
~ between(d2,d1,d3),
inference(res,[status(thm),theory(equality)],[66,86]),
[iquote('0:Res:66.1,86.0')] ).
cnf(182,plain,
colinear(d3,a,b),
inference(res,[status(thm),theory(equality)],[85,70]),
[iquote('0:Res:85.0,70.0')] ).
cnf(183,plain,
colinear(d2,a,b),
inference(res,[status(thm),theory(equality)],[84,70]),
[iquote('0:Res:84.0,70.0')] ).
cnf(184,plain,
colinear(d1,a,b),
inference(res,[status(thm),theory(equality)],[83,70]),
[iquote('0:Res:83.0,70.0')] ).
cnf(1132,plain,
( ~ colinear(u,a,b)
| equal(b,a)
| colinear(d3,u,a) ),
inference(res,[status(thm),theory(equality)],[182,81]),
[iquote('0:Res:182.0,81.0')] ).
cnf(1133,plain,
( ~ colinear(u,a,b)
| equal(b,a)
| colinear(d2,u,a) ),
inference(res,[status(thm),theory(equality)],[183,81]),
[iquote('0:Res:183.0,81.0')] ).
cnf(1146,plain,
( ~ colinear(u,a,b)
| colinear(d3,u,a) ),
inference(mrr,[status(thm)],[1132,82]),
[iquote('0:MRR:1132.1,82.0')] ).
cnf(1147,plain,
( ~ colinear(u,a,b)
| colinear(d2,u,a) ),
inference(mrr,[status(thm)],[1133,82]),
[iquote('0:MRR:1133.1,82.0')] ).
cnf(2005,plain,
colinear(d3,d2,a),
inference(res,[status(thm),theory(equality)],[183,1146]),
[iquote('0:Res:183.0,1146.0')] ).
cnf(2006,plain,
colinear(d3,d1,a),
inference(res,[status(thm),theory(equality)],[184,1146]),
[iquote('0:Res:184.0,1146.0')] ).
cnf(2012,plain,
( between(a,d3,d2)
| between(d2,a,d3)
| between(d3,d2,a) ),
inference(res,[status(thm),theory(equality)],[2005,108]),
[iquote('0:Res:2005.0,108.0')] ).
cnf(2030,plain,
colinear(d1,a,d3),
inference(res,[status(thm),theory(equality)],[2006,68]),
[iquote('0:Res:2006.0,68.0')] ).
cnf(2320,plain,
colinear(d2,d1,a),
inference(res,[status(thm),theory(equality)],[184,1147]),
[iquote('0:Res:184.0,1147.0')] ).
cnf(2355,plain,
colinear(d1,a,d2),
inference(res,[status(thm),theory(equality)],[2320,68]),
[iquote('0:Res:2320.0,68.0')] ).
cnf(9947,plain,
( ~ colinear(d1,a,d2)
| equal(d1,a) ),
inference(res,[status(thm),theory(equality)],[2030,117]),
[iquote('0:Res:2030.0,117.0')] ).
cnf(9952,plain,
equal(d1,a),
inference(mrr,[status(thm)],[9947,2355]),
[iquote('0:MRR:9947.0,2355.0')] ).
cnf(10001,plain,
~ between(a,d3,d2),
inference(rew,[status(thm),theory(equality)],[9952,114]),
[iquote('0:Rew:9952.0,114.0')] ).
cnf(10003,plain,
~ between(d3,d2,a),
inference(rew,[status(thm),theory(equality)],[9952,120]),
[iquote('0:Rew:9952.0,120.0')] ).
cnf(10005,plain,
~ between(d2,a,d3),
inference(rew,[status(thm),theory(equality)],[9952,125]),
[iquote('0:Rew:9952.0,125.0')] ).
cnf(10574,plain,
( between(d2,a,d3)
| between(d3,d2,a) ),
inference(mrr,[status(thm)],[2012,10001]),
[iquote('0:MRR:2012.0,10001.0')] ).
cnf(10581,plain,
$false,
inference(mrr,[status(thm)],[10574,10005,10003]),
[iquote('0:MRR:10574.0,10574.1,10005.0,10003.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : GEO013-3 : TPTP v8.1.0. Bugfixed v1.2.1.
% 0.06/0.13 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n012.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 07:53:38 EDT 2022
% 0.12/0.34 % CPUTime :
% 4.09/4.29
% 4.09/4.29 SPASS V 3.9
% 4.09/4.29 SPASS beiseite: Proof found.
% 4.09/4.29 % SZS status Theorem
% 4.09/4.29 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.09/4.29 SPASS derived 9440 clauses, backtracked 1941 clauses, performed 6 splits and kept 4927 clauses.
% 4.09/4.29 SPASS allocated 69192 KBytes.
% 4.09/4.29 SPASS spent 0:00:03.91 on the problem.
% 4.09/4.29 0:00:00.04 for the input.
% 4.09/4.29 0:00:00.00 for the FLOTTER CNF translation.
% 4.09/4.29 0:00:00.07 for inferences.
% 4.09/4.29 0:00:00.01 for the backtracking.
% 4.09/4.29 0:00:03.73 for the reduction.
% 4.09/4.29
% 4.09/4.29
% 4.09/4.29 Here is a proof with depth 5, length 37 :
% 4.09/4.29 % SZS output start Refutation
% See solution above
% 4.09/4.29 Formulae used in the proof : c2_1 c2_2 c2_3 t10_2 t10_4 t12_1 c5_2 a_not_b and1_colinear abd2_colinear abd3_colinear prove_d1d2d3_colinear colinearity4
% 4.09/4.29
%------------------------------------------------------------------------------