%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWV598-1 : TPTP v8.1.0. Released v4.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n009.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 : Wed Jul 20 21:44:31 EDT 2022
% Result : Unsatisfiable 0.92s 1.16s
% Output : Refutation 0.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 14
% Syntax : Number of clauses : 37 ( 25 unt; 2 nHn; 37 RR)
% Number of literals : 55 ( 0 equ; 27 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 8 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(111,axiom,
( ~ c_lessequals(u,v,tc_RealDef_Oreal)
| equal(u,v)
| c_HOL_Oord__class_Oless(u,v,tc_RealDef_Oreal) ),
file('SWV598-1.p',unknown),
[] ).
cnf(394,axiom,
equal(c_HOL_Otimes__class_Otimes(u,v,tc_RealDef_Oreal),c_HOL_Otimes__class_Otimes(v,u,tc_RealDef_Oreal)),
file('SWV598-1.p',unknown),
[] ).
cnf(529,axiom,
( ~ class_Orderings_Olinorder(u)
| c_lessequals(v,w,u)
| c_HOL_Oord__class_Oless(w,v,u) ),
file('SWV598-1.p',unknown),
[] ).
cnf(1029,axiom,
equal(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Otan(c_Transcendental_Opi)),
file('SWV598-1.p',unknown),
[] ).
cnf(1203,axiom,
equal(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Ocos(c_Transcendental_Osko__Transcendental__Xcos__is__zero__1__1)),
file('SWV598-1.p',unknown),
[] ).
cnf(1205,axiom,
equal(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Osin(c_Transcendental_Opi)),
file('SWV598-1.p',unknown),
[] ).
cnf(1216,axiom,
c_HOL_Oord__class_Oless(v_x,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal),
file('SWV598-1.p',unknown),
[] ).
cnf(1217,axiom,
c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_x,tc_RealDef_Oreal),
file('SWV598-1.p',unknown),
[] ).
cnf(1218,axiom,
( ~ equal(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Osin(v_x))
| ~ c_HOL_Oord__class_Oless(v_x,c_HOL_Otimes__class_Otimes(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),c_Transcendental_Opi,tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,v_x,tc_RealDef_Oreal) ),
file('SWV598-1.p',unknown),
[] ).
cnf(1219,axiom,
( ~ equal(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_Transcendental_Ocos(v_x))
| ~ equal(v_x,c_Transcendental_Opi) ),
file('SWV598-1.p',unknown),
[] ).
cnf(1220,axiom,
( ~ equal(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Osin(v_x))
| ~ c_HOL_Oord__class_Oless(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),v_x,tc_RealDef_Oreal) ),
file('SWV598-1.p',unknown),
[] ).
cnf(1287,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('SWV598-1.p',unknown),
[] ).
cnf(1329,axiom,
equal(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Osin(v_x)),
file('SWV598-1.p',unknown),
[] ).
cnf(1330,axiom,
equal(c_HOL_Oone__class_Oone(tc_RealDef_Oreal),c_Transcendental_Ocos(v_x)),
file('SWV598-1.p',unknown),
[] ).
cnf(1331,plain,
c_HOL_Oord__class_Oless(c_Transcendental_Osin(v_x),v_x,tc_RealDef_Oreal),
inference(rew,[status(thm),theory(equality)],[1329,1217]),
[iquote('0:Rew:1329.0,1217.0')] ).
cnf(1333,plain,
equal(c_Transcendental_Osin(v_x),c_Transcendental_Osin(c_Transcendental_Opi)),
inference(rew,[status(thm),theory(equality)],[1329,1205]),
[iquote('0:Rew:1329.0,1205.0')] ).
cnf(1334,plain,
equal(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Osin(c_Transcendental_Opi)),
inference(rew,[status(thm),theory(equality)],[1333,1329]),
[iquote('0:Rew:1333.0,1329.0')] ).
cnf(1335,plain,
c_HOL_Oord__class_Oless(c_Transcendental_Osin(c_Transcendental_Opi),v_x,tc_RealDef_Oreal),
inference(rew,[status(thm),theory(equality)],[1333,1331]),
[iquote('0:Rew:1333.0,1331.0')] ).
cnf(1339,plain,
equal(c_Transcendental_Ocos(c_Transcendental_Osko__Transcendental__Xcos__is__zero__1__1),c_Transcendental_Otan(c_Transcendental_Opi)),
inference(rew,[status(thm),theory(equality)],[1203,1029]),
[iquote('0:Rew:1203.0,1029.0')] ).
cnf(1340,plain,
equal(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Otan(c_Transcendental_Opi)),
inference(rew,[status(thm),theory(equality)],[1339,1203]),
[iquote('0:Rew:1339.0,1203.0')] ).
cnf(1345,plain,
equal(c_Transcendental_Osin(c_Transcendental_Opi),c_Transcendental_Otan(c_Transcendental_Opi)),
inference(rew,[status(thm),theory(equality)],[1334,1340]),
[iquote('0:Rew:1334.0,1340.0')] ).
cnf(1346,plain,
equal(c_Transcendental_Osin(v_x),c_Transcendental_Otan(c_Transcendental_Opi)),
inference(rew,[status(thm),theory(equality)],[1345,1333]),
[iquote('0:Rew:1345.0,1333.0')] ).
cnf(1347,plain,
equal(c_HOL_Ozero__class_Ozero(tc_RealDef_Oreal),c_Transcendental_Otan(c_Transcendental_Opi)),
inference(rew,[status(thm),theory(equality)],[1345,1334]),
[iquote('0:Rew:1345.0,1334.0')] ).
cnf(1348,plain,
c_HOL_Oord__class_Oless(c_Transcendental_Otan(c_Transcendental_Opi),v_x,tc_RealDef_Oreal),
inference(rew,[status(thm),theory(equality)],[1345,1335]),
[iquote('0:Rew:1345.0,1335.0')] ).
cnf(1387,plain,
( ~ equal(c_Transcendental_Ocos(v_x),c_Transcendental_Ocos(v_x))
| ~ equal(v_x,c_Transcendental_Opi) ),
inference(rew,[status(thm),theory(equality)],[1330,1219]),
[iquote('0:Rew:1330.0,1219.0')] ).
cnf(1388,plain,
~ equal(v_x,c_Transcendental_Opi),
inference(obv,[status(thm),theory(equality)],[1387]),
[iquote('0:Obv:1387.0')] ).
cnf(1406,plain,
c_HOL_Oord__class_Oless(v_x,c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal),
inference(rew,[status(thm),theory(equality)],[394,1216]),
[iquote('0:Rew:394.0,1216.0')] ).
cnf(1526,plain,
( ~ equal(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Otan(c_Transcendental_Opi))
| ~ c_HOL_Oord__class_Oless(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_Transcendental_Otan(c_Transcendental_Opi),v_x,tc_RealDef_Oreal) ),
inference(rew,[status(thm),theory(equality)],[1347,1220,1346]),
[iquote('0:Rew:1347.0,1220.2,1347.0,1220.0,1346.0,1220.0')] ).
cnf(1527,plain,
( ~ c_HOL_Oord__class_Oless(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_Transcendental_Otan(c_Transcendental_Opi),v_x,tc_RealDef_Oreal) ),
inference(obv,[status(thm),theory(equality)],[1526]),
[iquote('0:Obv:1526.0')] ).
cnf(1528,plain,
~ c_HOL_Oord__class_Oless(v_x,c_Transcendental_Opi,tc_RealDef_Oreal),
inference(mrr,[status(thm)],[1527,1348]),
[iquote('0:MRR:1527.1,1348.0')] ).
cnf(1615,plain,
( ~ equal(c_Transcendental_Otan(c_Transcendental_Opi),c_Transcendental_Otan(c_Transcendental_Opi))
| ~ c_HOL_Oord__class_Oless(v_x,c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,v_x,tc_RealDef_Oreal) ),
inference(rew,[status(thm),theory(equality)],[394,1218,1347,1346]),
[iquote('0:Rew:394.0,1218.1,1347.0,1218.0,1346.0,1218.0')] ).
cnf(1616,plain,
( ~ c_HOL_Oord__class_Oless(v_x,c_HOL_Otimes__class_Otimes(c_Transcendental_Opi,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_RealDef_Oreal),tc_RealDef_Oreal),tc_RealDef_Oreal)
| ~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,v_x,tc_RealDef_Oreal) ),
inference(obv,[status(thm),theory(equality)],[1615]),
[iquote('0:Obv:1615.0')] ).
cnf(1617,plain,
~ c_HOL_Oord__class_Oless(c_Transcendental_Opi,v_x,tc_RealDef_Oreal),
inference(mrr,[status(thm)],[1616,1406]),
[iquote('0:MRR:1616.0,1406.0')] ).
cnf(1993,plain,
( ~ c_lessequals(v_x,c_Transcendental_Opi,tc_RealDef_Oreal)
| equal(v_x,c_Transcendental_Opi) ),
inference(res,[status(thm),theory(equality)],[111,1528]),
[iquote('0:Res:111.1,1528.0')] ).
cnf(2052,plain,
( ~ class_Orderings_Olinorder(tc_RealDef_Oreal)
| c_lessequals(v_x,c_Transcendental_Opi,tc_RealDef_Oreal) ),
inference(res,[status(thm),theory(equality)],[529,1617]),
[iquote('0:Res:529.1,1617.0')] ).
cnf(5316,plain,
c_lessequals(v_x,c_Transcendental_Opi,tc_RealDef_Oreal),
inference(mrr,[status(thm)],[2052,1287]),
[iquote('0:MRR:2052.0,1287.0')] ).
cnf(5322,plain,
$false,
inference(mrr,[status(thm)],[1993,5316,1388]),
[iquote('0:MRR:1993.0,1993.1,5316.0,1388.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV598-1 : TPTP v8.1.0. Released v4.1.0.
% 0.12/0.13 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n009.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 : Wed Jun 15 02:04:23 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.92/1.16
% 0.92/1.16 SPASS V 3.9
% 0.92/1.16 SPASS beiseite: Proof found.
% 0.92/1.16 % SZS status Theorem
% 0.92/1.16 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.92/1.16 SPASS derived 1197 clauses, backtracked 0 clauses, performed 0 splits and kept 1254 clauses.
% 0.92/1.16 SPASS allocated 79258 KBytes.
% 0.92/1.16 SPASS spent 0:00:00.78 on the problem.
% 0.92/1.16 0:00:00.12 for the input.
% 0.92/1.16 0:00:00.00 for the FLOTTER CNF translation.
% 0.92/1.16 0:00:00.00 for inferences.
% 0.92/1.16 0:00:00.00 for the backtracking.
% 0.92/1.16 0:00:00.33 for the reduction.
% 0.92/1.16
% 0.92/1.16
% 0.92/1.16 Here is a proof with depth 1, length 37 :
% 0.92/1.16 % SZS output start Refutation
% See solution above
% 0.92/1.16 Formulae used in the proof : cls_real__less__def_2 cls_real__mult__commute_0 cls_linorder__not__le_0 cls_tan__pi_0 cls_cos__is__zero_2 cls_sin__pi_0 cls_CHAINED_0 cls_CHAINED_0_01 cls_CHAINED_0_02 cls_CHAINED_0_03 cls_CHAINED_0_04 clsarity_RealDef__Oreal__Orderings_Olinorder cls_conjecture_0 cls_conjecture_1
% 0.92/1.16
%------------------------------------------------------------------------------