%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : ALG402-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:48:26 AM UTC 2026
% Result : Unsatisfiable 159.37s 23.24s
% Output : CNFRefutation 159.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 15
% Syntax : Number of clauses : 55 ( 32 unt; 2 nHn; 22 RR)
% Number of literals : 87 ( 35 equ; 34 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 4 con; 0-3 aty)
% Number of variables : 84 ( 19 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_dvd__0__left_0,axiom,
( ~ 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'('c$uHOL$uOzero$u$uclass$uOzero'(X0),X1,X0)
| X1 = 'c$uHOL$uOzero$u$uclass$uOzero'(X0)
| ~ 'class$uRing$u$uand$u$uField$uOcomm$u$usemiring$u$u1'(X0) ) ).
cnf(cls_gr0I_0,axiom,
( X0 = 'c$uHOL$uOzero$u$uclass$uOzero'('tc$unat')
| 'c$uHOL$uOord$u$uclass$uOless'('c$uHOL$uOzero$u$uclass$uOzero'('tc$unat'),X0,'tc$unat') ) ).
cnf(cls_dvd__trans_0,axiom,
( ~ 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X1,X3,X0)
| ~ 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X3,X2,X0)
| 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X1,X2,X0)
| ~ 'class$uRing$u$uand$u$uField$uOcomm$u$usemiring$u$u1'(X0) ) ).
cnf(cls_one__dvd_0,axiom,
( 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'('c$uHOL$uOone$u$uclass$uOone'(X0),X1,X0)
| ~ 'class$uRing$u$uand$u$uField$uOcomm$u$usemiring$u$u1'(X0) ) ).
cnf(cls_dvd__power_0,axiom,
( ~ 'c$uHOL$uOord$u$uclass$uOless'('c$uHOL$uOzero$u$uclass$uOzero'('tc$unat'),X2,'tc$unat')
| 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X1,'c$uPower$uOpower$u$uclass$uOpower'(X1,X2,X0),X0)
| ~ 'class$uRing$u$uand$u$uField$uOcomm$u$usemiring$u$u1'(X0) ) ).
cnf(cls_power__one_0,axiom,
( 'c$uPower$uOpower$u$uclass$uOpower'('c$uHOL$uOone$u$uclass$uOone'(X0),X1,X0) = 'c$uHOL$uOone$u$uclass$uOone'(X0)
| ~ 'class$uOrderedGroup$uOmonoid$u$umult'(X0) ) ).
cnf(cls_Suc__diff__1_0,axiom,
( ~ 'c$uHOL$uOord$u$uclass$uOless'('c$uHOL$uOzero$u$uclass$uOzero'('tc$unat'),X0,'tc$unat')
| 'c$uSuc'('c$uHOL$uOminus$u$uclass$uOminus'(X0,'c$uHOL$uOone$u$uclass$uOone'('tc$unat'),'tc$unat')) = X0 ) ).
cnf(cls_One__nat__def_0,axiom,
'c$uHOL$uOone$u$uclass$uOone'('tc$unat') = 'c$uSuc'('c$uHOL$uOzero$u$uclass$uOzero'('tc$unat')) ).
cnf(cls_class__semiring_Osemiring__rules_I28_J_0,axiom,
( 'c$uHOL$uOtimes$u$uclass$uOtimes'('c$uPower$uOpower$u$uclass$uOpower'(X1,X2,X0),X1,X0) = 'c$uPower$uOpower$u$uclass$uOpower'(X1,'c$uSuc'(X2),X0)
| ~ 'class$uRing$u$uand$u$uField$uOcomm$u$usemiring$u$u1'(X0) ) ).
cnf(cls_kas_I1_J_0,axiom,
'v$ua' != 'c$uHOL$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') ).
cnf(cls_kas_I2_J_0,axiom,
'v$uk' != 'c$uHOL$uOzero$u$uclass$uOzero'('tc$unat') ).
cnf(cls_class__semiring_Omul__c_0,axiom,
( 'c$uHOL$uOtimes$u$uclass$uOtimes'(X1,X2,X0) = 'c$uHOL$uOtimes$u$uclass$uOtimes'(X2,X1,X0)
| ~ 'class$uRing$u$uand$u$uField$uOcomm$u$usemiring$u$u1'(X0) ) ).
cnf(cls_conjecture_0,negated_conjecture,
'c$uHOL$uOtimes$u$uclass$uOtimes'(X0,'c$uPower$uOpower$u$uclass$uOpower'(X0,'c$uHOL$uOminus$u$uclass$uOminus'('v$uk','c$uSuc'('c$uHOL$uOzero$u$uclass$uOzero'('tc$unat')),'tc$unat'),'tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex') = 'c$uHOL$uOtimes$u$uclass$uOtimes'(X1,'c$uPower$uOpower$u$uclass$uOpower'(X1,'c$uHOL$uOminus$u$uclass$uOminus'('v$uk','c$uSuc'('c$uHOL$uOzero$u$uclass$uOzero'('tc$unat')),'tc$unat'),'tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex') ).
cnf(clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1,axiom,
'class$uRing$u$uand$u$uField$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex') ).
cnf(clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__mult,axiom,
'class$uOrderedGroup$uOmonoid$u$umult'('tc$uComplex$uOcomplex') ).
cnf(c78,plain,
( ~ 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'('c$uHOL$uOzero$u$uclass$uOzero'(X0),X1,X0)
| ~ 'class$uRing$u$uand$u$uField$uOcomm$u$usemiring$u$u1'(X0)
| 'c$uHOL$uOzero$u$uclass$uOzero'(X0) = X1 ),
inference(clausification,[status(esa)],[cls_dvd__0__left_0]) ).
cnf(c318,plain,
( 'c$uHOL$uOzero$u$uclass$uOzero'('tc$unat') = X0
| 'c$uHOL$uOord$u$uclass$uOless'('c$uHOL$uOzero$u$uclass$uOzero'('tc$unat'),X0,'tc$unat') ),
inference(clausification,[status(esa)],[cls_gr0I_0]) ).
cnf(c331,plain,
( ~ 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X3,X0,X2)
| 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X3,X1,X2)
| ~ 'class$uRing$u$uand$u$uField$uOcomm$u$usemiring$u$u1'(X2)
| ~ 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X0,X1,X2) ),
inference(clausification,[status(esa)],[cls_dvd__trans_0]) ).
cnf(c347,plain,
( 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'('c$uHOL$uOone$u$uclass$uOone'(X0),X1,X0)
| ~ 'class$uRing$u$uand$u$uField$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[cls_one__dvd_0]) ).
cnf(c433,plain,
( ~ 'c$uHOL$uOord$u$uclass$uOless'('c$uHOL$uOzero$u$uclass$uOzero'('tc$unat'),X1,'tc$unat')
| ~ 'class$uRing$u$uand$u$uField$uOcomm$u$usemiring$u$u1'(X2)
| 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X0,'c$uPower$uOpower$u$uclass$uOpower'(X0,X1,X2),X2) ),
inference(clausification,[status(esa)],[cls_dvd__power_0]) ).
cnf(c446,plain,
( 'c$uHOL$uOone$u$uclass$uOone'(X0) = 'c$uPower$uOpower$u$uclass$uOpower'('c$uHOL$uOone$u$uclass$uOone'(X0),X1,X0)
| ~ 'class$uOrderedGroup$uOmonoid$u$umult'(X0) ),
inference(clausification,[status(esa)],[cls_power__one_0]) ).
cnf(c506,plain,
( ~ 'c$uHOL$uOord$u$uclass$uOless'('c$uHOL$uOzero$u$uclass$uOzero'('tc$unat'),X0,'tc$unat')
| 'c$uSuc'('c$uHOL$uOminus$u$uclass$uOminus'(X0,'c$uHOL$uOone$u$uclass$uOone'('tc$unat'),'tc$unat')) = X0 ),
inference(clausification,[status(esa)],[cls_Suc__diff__1_0]) ).
cnf(c715,plain,
'c$uSuc'('c$uHOL$uOzero$u$uclass$uOzero'('tc$unat')) = 'c$uHOL$uOone$u$uclass$uOone'('tc$unat'),
inference(clausification,[status(esa)],[cls_One__nat__def_0]) ).
cnf(c857,plain,
( 'c$uPower$uOpower$u$uclass$uOpower'(X1,'c$uSuc'(X2),X0) = 'c$uHOL$uOtimes$u$uclass$uOtimes'('c$uPower$uOpower$u$uclass$uOpower'(X1,X2,X0),X1,X0)
| ~ 'class$uRing$u$uand$u$uField$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[cls_class__semiring_Osemiring__rules_I28_J_0]) ).
cnf(c876,plain,
'c$uHOL$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') != 'v$ua',
inference(clausification,[status(esa)],[cls_kas_I1_J_0]) ).
cnf(c878,plain,
'v$uk' != 'c$uHOL$uOzero$u$uclass$uOzero'('tc$unat'),
inference(clausification,[status(esa)],[cls_kas_I2_J_0]) ).
cnf(c916,plain,
( 'c$uHOL$uOtimes$u$uclass$uOtimes'(X1,X2,X0) = 'c$uHOL$uOtimes$u$uclass$uOtimes'(X2,X1,X0)
| ~ 'class$uRing$u$uand$u$uField$uOcomm$u$usemiring$u$u1'(X0) ),
inference(clausification,[status(esa)],[cls_class__semiring_Omul__c_0]) ).
cnf(c930,plain,
'c$uHOL$uOtimes$u$uclass$uOtimes'(X0,'c$uPower$uOpower$u$uclass$uOpower'(X0,'c$uHOL$uOminus$u$uclass$uOminus'('v$uk','c$uSuc'('c$uHOL$uOzero$u$uclass$uOzero'('tc$unat')),'tc$unat'),'tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex') = 'c$uHOL$uOtimes$u$uclass$uOtimes'(X1,'c$uPower$uOpower$u$uclass$uOpower'(X1,'c$uHOL$uOminus$u$uclass$uOminus'('v$uk','c$uSuc'('c$uHOL$uOzero$u$uclass$uOzero'('tc$unat')),'tc$unat'),'tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex'),
inference(clausification,[status(esa)],[cls_conjecture_0]) ).
cnf(c1018,plain,
'class$uRing$u$uand$u$uField$uOcomm$u$usemiring$u$u1'('tc$uComplex$uOcomplex'),
inference(clausification,[status(esa)],[clsarity_Complex__Ocomplex__Ring__and__Field_Ocomm__semiring__1]) ).
cnf(c1033,plain,
'class$uOrderedGroup$uOmonoid$u$umult'('tc$uComplex$uOcomplex'),
inference(clausification,[status(esa)],[clsarity_Complex__Ocomplex__OrderedGroup_Omonoid__mult]) ).
cnf(d0,plain,
( ~ 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'('c$uHOL$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex'),X0,'tc$uComplex$uOcomplex')
| 'c$uHOL$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = X0 ),
inference(resolution,[status(thm)],[c1018,c78]) ).
cnf(d1,plain,
'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'('c$uHOL$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'),X0,'tc$uComplex$uOcomplex'),
inference(resolution,[status(thm)],[c347,c1018]) ).
cnf(d2,plain,
( ~ 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X2,X1,'tc$uComplex$uOcomplex')
| ~ 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X0,X2,'tc$uComplex$uOcomplex')
| 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X0,X1,'tc$uComplex$uOcomplex') ),
inference(resolution,[status(thm)],[c331,c1018]) ).
cnf(d3,plain,
( 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X0,X1,'tc$uComplex$uOcomplex')
| ~ 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X0,'c$uHOL$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex') ),
inference(resolution,[status(thm)],[d2,d1]) ).
cnf(d4,plain,
( 'c$uHOL$uOord$u$uclass$uOless'('c$uHOL$uOzero$u$uclass$uOzero'('tc$unat'),X0,'tc$unat')
| 'v$uk' != X0 ),
inference(superposition,[status(thm)],[c318,c878]) ).
cnf(d5,plain,
'c$uHOL$uOord$u$uclass$uOless'('c$uHOL$uOzero$u$uclass$uOzero'('tc$unat'),'v$uk','tc$unat'),
inference(equality_resolution,[status(thm)],[d4]) ).
cnf(d6,plain,
( 'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X1,'c$uPower$uOpower$u$uclass$uOpower'(X1,'v$uk',X0),X0)
| ~ 'class$uRing$u$uand$u$uField$uOcomm$u$usemiring$u$u1'(X0) ),
inference(resolution,[status(thm)],[c433,d5]) ).
cnf(d7,plain,
'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X0,'c$uPower$uOpower$u$uclass$uOpower'(X0,'v$uk','tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex'),
inference(resolution,[status(thm)],[d6,c1018]) ).
cnf(d8,plain,
'c$uSuc'('c$uHOL$uOminus$u$uclass$uOminus'('v$uk','c$uHOL$uOone$u$uclass$uOone'('tc$unat'),'tc$unat')) = 'v$uk',
inference(resolution,[status(thm)],[c506,d5]) ).
cnf(d9,plain,
'c$uHOL$uOtimes$u$uclass$uOtimes'(X0,X1,'tc$uComplex$uOcomplex') = 'c$uHOL$uOtimes$u$uclass$uOtimes'(X1,X0,'tc$uComplex$uOcomplex'),
inference(resolution,[status(thm)],[c916,c1018]) ).
cnf(d10,plain,
'c$uPower$uOpower$u$uclass$uOpower'(X0,'c$uSuc'(X1),'tc$uComplex$uOcomplex') = 'c$uHOL$uOtimes$u$uclass$uOtimes'('c$uPower$uOpower$u$uclass$uOpower'(X0,X1,'tc$uComplex$uOcomplex'),X0,'tc$uComplex$uOcomplex'),
inference(resolution,[status(thm)],[c857,c1018]) ).
cnf(d11,plain,
'c$uPower$uOpower$u$uclass$uOpower'(X0,'c$uSuc'(X1),'tc$uComplex$uOcomplex') = 'c$uHOL$uOtimes$u$uclass$uOtimes'(X0,'c$uPower$uOpower$u$uclass$uOpower'(X0,X1,'tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex'),
inference(demodulation,[status(thm)],[d10,d9]) ).
cnf(d12,plain,
'c$uHOL$uOtimes$u$uclass$uOtimes'(X0,'c$uPower$uOpower$u$uclass$uOpower'(X0,'c$uHOL$uOminus$u$uclass$uOminus'('v$uk','c$uHOL$uOone$u$uclass$uOone'('tc$unat'),'tc$unat'),'tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex') = 'c$uHOL$uOtimes$u$uclass$uOtimes'(X1,'c$uPower$uOpower$u$uclass$uOpower'(X1,'c$uHOL$uOminus$u$uclass$uOminus'('v$uk','c$uSuc'('c$uHOL$uOzero$u$uclass$uOzero'('tc$unat')),'tc$unat'),'tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex'),
inference(demodulation,[status(thm)],[c930,c715]) ).
cnf(d13,plain,
'c$uHOL$uOtimes$u$uclass$uOtimes'(X0,'c$uPower$uOpower$u$uclass$uOpower'(X0,'c$uHOL$uOminus$u$uclass$uOminus'('v$uk','c$uHOL$uOone$u$uclass$uOone'('tc$unat'),'tc$unat'),'tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex') = 'c$uHOL$uOtimes$u$uclass$uOtimes'(X1,'c$uPower$uOpower$u$uclass$uOpower'(X1,'c$uHOL$uOminus$u$uclass$uOminus'('v$uk','c$uHOL$uOone$u$uclass$uOone'('tc$unat'),'tc$unat'),'tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex'),
inference(demodulation,[status(thm)],[d12,c715]) ).
cnf(d14,plain,
'c$uHOL$uOtimes$u$uclass$uOtimes'(X2,'c$uPower$uOpower$u$uclass$uOpower'(X2,'c$uHOL$uOminus$u$uclass$uOminus'('v$uk','c$uHOL$uOone$u$uclass$uOone'('tc$unat'),'tc$unat'),'tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex') = 'c$uHOL$uOtimes$u$uclass$uOtimes'(X1,'c$uPower$uOpower$u$uclass$uOpower'(X1,'c$uHOL$uOminus$u$uclass$uOminus'('v$uk','c$uHOL$uOone$u$uclass$uOone'('tc$unat'),'tc$unat'),'tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex'),
inference(superposition,[status(thm)],[d13,d13]) ).
cnf(d15,plain,
'c$uPower$uOpower$u$uclass$uOpower'(X0,'c$uSuc'('c$uHOL$uOminus$u$uclass$uOminus'('v$uk','c$uHOL$uOone$u$uclass$uOone'('tc$unat'),'tc$unat')),'tc$uComplex$uOcomplex') = 'c$uHOL$uOtimes$u$uclass$uOtimes'(X1,'c$uPower$uOpower$u$uclass$uOpower'(X1,'c$uHOL$uOminus$u$uclass$uOminus'('v$uk','c$uHOL$uOone$u$uclass$uOone'('tc$unat'),'tc$unat'),'tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex'),
inference(demodulation,[status(thm)],[d14,d11]) ).
cnf(d16,plain,
'c$uPower$uOpower$u$uclass$uOpower'(X0,'v$uk','tc$uComplex$uOcomplex') = 'c$uHOL$uOtimes$u$uclass$uOtimes'(X1,'c$uPower$uOpower$u$uclass$uOpower'(X1,'c$uHOL$uOminus$u$uclass$uOminus'('v$uk','c$uHOL$uOone$u$uclass$uOone'('tc$unat'),'tc$unat'),'tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex'),
inference(demodulation,[status(thm)],[d15,d8]) ).
cnf(d17,plain,
'c$uPower$uOpower$u$uclass$uOpower'(X1,'v$uk','tc$uComplex$uOcomplex') = 'c$uPower$uOpower$u$uclass$uOpower'(X0,'c$uSuc'('c$uHOL$uOminus$u$uclass$uOminus'('v$uk','c$uHOL$uOone$u$uclass$uOone'('tc$unat'),'tc$unat')),'tc$uComplex$uOcomplex'),
inference(demodulation,[status(thm)],[d16,d11]) ).
cnf(d18,plain,
'c$uPower$uOpower$u$uclass$uOpower'(X0,'v$uk','tc$uComplex$uOcomplex') = 'c$uPower$uOpower$u$uclass$uOpower'(X1,'v$uk','tc$uComplex$uOcomplex'),
inference(demodulation,[status(thm)],[d17,d8]) ).
cnf(d19,plain,
'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X0,'c$uPower$uOpower$u$uclass$uOpower'(X1,'v$uk','tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex'),
inference(superposition,[status(thm)],[d18,d7]) ).
cnf(d20,plain,
'c$uHOL$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex') = 'c$uPower$uOpower$u$uclass$uOpower'('c$uHOL$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'),X0,'tc$uComplex$uOcomplex'),
inference(resolution,[status(thm)],[c446,c1033]) ).
cnf(d21,plain,
'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X0,'c$uHOL$uOone$u$uclass$uOone'('tc$uComplex$uOcomplex'),'tc$uComplex$uOcomplex'),
inference(superposition,[status(thm)],[d20,d19]) ).
cnf(d22,plain,
'c$uRing$u$uand$u$uField$uOdvd$u$uclass$uOdvd'(X0,X1,'tc$uComplex$uOcomplex'),
inference(resolution,[status(thm)],[d21,d3]) ).
cnf(d23,plain,
'c$uHOL$uOzero$u$uclass$uOzero'('tc$uComplex$uOcomplex') = X0,
inference(resolution,[status(thm)],[d22,d0]) ).
cnf(d24,plain,
$false,
inference(resolution,[status(thm)],[d23,c876]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG402-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.39 % Computer : n001.cluster.edu
% 0.09/0.39 % Model : x86_64 x86_64
% 0.09/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.39 % Memory : 8046.5625MB
% 0.09/0.39 % OS : Linux 6.8.0-71-generic
% 0.09/0.39 % CPULimit : 300
% 0.09/0.39 % WCLimit : 300
% 0.09/0.39 % DateTime : Sat Sep 26 22:03:44 UTC 2026
% 0.09/0.39 % CPUTime :
% 0.09/0.39 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 159.37/23.24 % SZS status Unsatisfiable for theBenchmark.p
% 159.37/23.24 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------