%------------------------------------------------------------------------------
% File : Mace4---2026-6A
% Problem : SWV595-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : mace4 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 09:06:08 AM UTC 2026
% Result : Satisfiable 0.14s 5.55s
% Output : FiniteModel 0.14s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(interp_domain,interpretation-domains,
! [X] :
( X = "d2"
| X = "d1"
| X = "d0" ) ).
fof(interp_functions,interpretation-mappings,
( c_RealVector_OscaleR__class_OscaleR("d2","d2","d2") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d2","d2","d1") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d2","d2","d0") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d2","d1","d2") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d2","d1","d1") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d2","d1","d0") = "d1"
& c_RealVector_OscaleR__class_OscaleR("d2","d0","d2") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d2","d0","d1") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d2","d0","d0") = "d2"
& c_RealVector_OscaleR__class_OscaleR("d1","d2","d2") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d1","d2","d1") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d1","d2","d0") = "d1"
& c_RealVector_OscaleR__class_OscaleR("d1","d1","d2") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d1","d1","d1") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d1","d1","d0") = "d1"
& c_RealVector_OscaleR__class_OscaleR("d1","d0","d2") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d1","d0","d1") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d1","d0","d0") = "d1"
& c_RealVector_OscaleR__class_OscaleR("d0","d2","d2") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d0","d2","d1") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d0","d2","d0") = "d2"
& c_RealVector_OscaleR__class_OscaleR("d0","d1","d2") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d0","d1","d1") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d0","d1","d0") = "d1"
& c_RealVector_OscaleR__class_OscaleR("d0","d0","d2") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d0","d0","d1") = "d0"
& c_RealVector_OscaleR__class_OscaleR("d0","d0","d0") = "d0"
& c_Power_Opower__class_Opower("d2","d2","d2") = "d0"
& c_Power_Opower__class_Opower("d2","d2","d1") = "d0"
& c_Power_Opower__class_Opower("d2","d2","d0") = "d0"
& c_Power_Opower__class_Opower("d2","d1","d2") = "d0"
& c_Power_Opower__class_Opower("d2","d1","d1") = "d0"
& c_Power_Opower__class_Opower("d2","d1","d0") = "d0"
& c_Power_Opower__class_Opower("d2","d0","d2") = "d0"
& c_Power_Opower__class_Opower("d2","d0","d1") = "d0"
& c_Power_Opower__class_Opower("d2","d0","d0") = "d0"
& c_Power_Opower__class_Opower("d1","d2","d2") = "d0"
& c_Power_Opower__class_Opower("d1","d2","d1") = "d0"
& c_Power_Opower__class_Opower("d1","d2","d0") = "d0"
& c_Power_Opower__class_Opower("d1","d1","d2") = "d0"
& c_Power_Opower__class_Opower("d1","d1","d1") = "d0"
& c_Power_Opower__class_Opower("d1","d1","d0") = "d0"
& c_Power_Opower__class_Opower("d1","d0","d2") = "d0"
& c_Power_Opower__class_Opower("d1","d0","d1") = "d0"
& c_Power_Opower__class_Opower("d1","d0","d0") = "d0"
& c_Power_Opower__class_Opower("d0","d2","d2") = "d0"
& c_Power_Opower__class_Opower("d0","d2","d1") = "d0"
& c_Power_Opower__class_Opower("d0","d2","d0") = "d0"
& c_Power_Opower__class_Opower("d0","d1","d2") = "d0"
& c_Power_Opower__class_Opower("d0","d1","d1") = "d0"
& c_Power_Opower__class_Opower("d0","d1","d0") = "d0"
& c_Power_Opower__class_Opower("d0","d0","d2") = "d0"
& c_Power_Opower__class_Opower("d0","d0","d1") = "d0"
& c_Power_Opower__class_Opower("d0","d0","d0") = "d0"
& c_HOL_Otimes__class_Otimes("d2","d2","d2") = "d0"
& c_HOL_Otimes__class_Otimes("d2","d2","d1") = "d0"
& c_HOL_Otimes__class_Otimes("d2","d2","d0") = "d0"
& c_HOL_Otimes__class_Otimes("d2","d1","d2") = "d0"
& c_HOL_Otimes__class_Otimes("d2","d1","d1") = "d0"
& c_HOL_Otimes__class_Otimes("d2","d1","d0") = "d1"
& c_HOL_Otimes__class_Otimes("d2","d0","d2") = "d0"
& c_HOL_Otimes__class_Otimes("d2","d0","d1") = "d0"
& c_HOL_Otimes__class_Otimes("d2","d0","d0") = "d2"
& c_HOL_Otimes__class_Otimes("d1","d2","d2") = "d0"
& c_HOL_Otimes__class_Otimes("d1","d2","d1") = "d0"
& c_HOL_Otimes__class_Otimes("d1","d2","d0") = "d1"
& c_HOL_Otimes__class_Otimes("d1","d1","d2") = "d0"
& c_HOL_Otimes__class_Otimes("d1","d1","d1") = "d0"
& c_HOL_Otimes__class_Otimes("d1","d1","d0") = "d1"
& c_HOL_Otimes__class_Otimes("d1","d0","d2") = "d0"
& c_HOL_Otimes__class_Otimes("d1","d0","d1") = "d0"
& c_HOL_Otimes__class_Otimes("d1","d0","d0") = "d1"
& c_HOL_Otimes__class_Otimes("d0","d2","d2") = "d0"
& c_HOL_Otimes__class_Otimes("d0","d2","d1") = "d0"
& c_HOL_Otimes__class_Otimes("d0","d2","d0") = "d2"
& c_HOL_Otimes__class_Otimes("d0","d1","d2") = "d0"
& c_HOL_Otimes__class_Otimes("d0","d1","d1") = "d0"
& c_HOL_Otimes__class_Otimes("d0","d1","d0") = "d1"
& c_HOL_Otimes__class_Otimes("d0","d0","d2") = "d0"
& c_HOL_Otimes__class_Otimes("d0","d0","d1") = "d0"
& c_HOL_Otimes__class_Otimes("d0","d0","d0") = "d0"
& c_HOL_Oinverse__class_Odivide("d2","d2","d2") = "d0"
& c_HOL_Oinverse__class_Odivide("d2","d2","d1") = "d0"
& c_HOL_Oinverse__class_Odivide("d2","d2","d0") = "d0"
& c_HOL_Oinverse__class_Odivide("d2","d1","d2") = "d0"
& c_HOL_Oinverse__class_Odivide("d2","d1","d1") = "d0"
& c_HOL_Oinverse__class_Odivide("d2","d1","d0") = "d1"
& c_HOL_Oinverse__class_Odivide("d2","d0","d2") = "d0"
& c_HOL_Oinverse__class_Odivide("d2","d0","d1") = "d0"
& c_HOL_Oinverse__class_Odivide("d2","d0","d0") = "d2"
& c_HOL_Oinverse__class_Odivide("d1","d2","d2") = "d0"
& c_HOL_Oinverse__class_Odivide("d1","d2","d1") = "d0"
& c_HOL_Oinverse__class_Odivide("d1","d2","d0") = "d1"
& c_HOL_Oinverse__class_Odivide("d1","d1","d2") = "d0"
& c_HOL_Oinverse__class_Odivide("d1","d1","d1") = "d0"
& c_HOL_Oinverse__class_Odivide("d1","d1","d0") = "d1"
& c_HOL_Oinverse__class_Odivide("d1","d0","d2") = "d0"
& c_HOL_Oinverse__class_Odivide("d1","d0","d1") = "d0"
& c_HOL_Oinverse__class_Odivide("d1","d0","d0") = "d1"
& c_HOL_Oinverse__class_Odivide("d0","d2","d2") = "d0"
& c_HOL_Oinverse__class_Odivide("d0","d2","d1") = "d0"
& c_HOL_Oinverse__class_Odivide("d0","d2","d0") = "d2"
& c_HOL_Oinverse__class_Odivide("d0","d1","d2") = "d0"
& c_HOL_Oinverse__class_Odivide("d0","d1","d1") = "d0"
& c_HOL_Oinverse__class_Odivide("d0","d1","d0") = "d1"
& c_HOL_Oinverse__class_Odivide("d0","d0","d2") = "d0"
& c_HOL_Oinverse__class_Odivide("d0","d0","d1") = "d0"
& c_HOL_Oinverse__class_Odivide("d0","d0","d0") = "d0"
& c_Divides_Odiv__class_Odiv("d2","d2","d2") = "d0"
& c_Divides_Odiv__class_Odiv("d2","d2","d1") = "d0"
& c_Divides_Odiv__class_Odiv("d2","d2","d0") = "d0"
& c_Divides_Odiv__class_Odiv("d2","d1","d2") = "d0"
& c_Divides_Odiv__class_Odiv("d2","d1","d1") = "d0"
& c_Divides_Odiv__class_Odiv("d2","d1","d0") = "d0"
& c_Divides_Odiv__class_Odiv("d2","d0","d2") = "d0"
& c_Divides_Odiv__class_Odiv("d2","d0","d1") = "d0"
& c_Divides_Odiv__class_Odiv("d2","d0","d0") = "d0"
& c_Divides_Odiv__class_Odiv("d1","d2","d2") = "d0"
& c_Divides_Odiv__class_Odiv("d1","d2","d1") = "d0"
& c_Divides_Odiv__class_Odiv("d1","d2","d0") = "d0"
& c_Divides_Odiv__class_Odiv("d1","d1","d2") = "d0"
& c_Divides_Odiv__class_Odiv("d1","d1","d1") = "d0"
& c_Divides_Odiv__class_Odiv("d1","d1","d0") = "d0"
& c_Divides_Odiv__class_Odiv("d1","d0","d2") = "d0"
& c_Divides_Odiv__class_Odiv("d1","d0","d1") = "d0"
& c_Divides_Odiv__class_Odiv("d1","d0","d0") = "d0"
& c_Divides_Odiv__class_Odiv("d0","d2","d2") = "d0"
& c_Divides_Odiv__class_Odiv("d0","d2","d1") = "d0"
& c_Divides_Odiv__class_Odiv("d0","d2","d0") = "d0"
& c_Divides_Odiv__class_Odiv("d0","d1","d2") = "d0"
& c_Divides_Odiv__class_Odiv("d0","d1","d1") = "d0"
& c_Divides_Odiv__class_Odiv("d0","d1","d0") = "d0"
& c_Divides_Odiv__class_Odiv("d0","d0","d2") = "d0"
& c_Divides_Odiv__class_Odiv("d0","d0","d1") = "d0"
& c_Divides_Odiv__class_Odiv("d0","d0","d0") = "d0"
& c_RealVector_Oof__real("d2","d2") = "d0"
& c_RealVector_Oof__real("d2","d1") = "d0"
& c_RealVector_Oof__real("d2","d0") = "d2"
& c_RealVector_Oof__real("d1","d2") = "d0"
& c_RealVector_Oof__real("d1","d1") = "d0"
& c_RealVector_Oof__real("d1","d0") = "d1"
& c_RealVector_Oof__real("d0","d2") = "d0"
& c_RealVector_Oof__real("d0","d1") = "d0"
& c_RealVector_Oof__real("d0","d0") = "d0"
& c_RealVector_Onorm__class_Onorm("d2","d2") = "d0"
& c_RealVector_Onorm__class_Onorm("d2","d1") = "d0"
& c_RealVector_Onorm__class_Onorm("d2","d0") = "d0"
& c_RealVector_Onorm__class_Onorm("d1","d2") = "d0"
& c_RealVector_Onorm__class_Onorm("d1","d1") = "d0"
& c_RealVector_Onorm__class_Onorm("d1","d0") = "d1"
& c_RealVector_Onorm__class_Onorm("d0","d2") = "d0"
& c_RealVector_Onorm__class_Onorm("d0","d1") = "d0"
& c_RealVector_Onorm__class_Onorm("d0","d0") = "d0"
& c_Log_Opowr("d2","d2") = "d0"
& c_Log_Opowr("d2","d1") = "d0"
& c_Log_Opowr("d2","d0") = "d0"
& c_Log_Opowr("d1","d2") = "d0"
& c_Log_Opowr("d1","d1") = "d0"
& c_Log_Opowr("d1","d0") = "d0"
& c_Log_Opowr("d0","d2") = "d0"
& c_Log_Opowr("d0","d1") = "d0"
& c_Log_Opowr("d0","d0") = "d0"
& c_HOL_Ouminus__class_Ouminus("d2","d2") = "d0"
& c_HOL_Ouminus__class_Ouminus("d2","d1") = "d0"
& c_HOL_Ouminus__class_Ouminus("d2","d0") = "d0"
& c_HOL_Ouminus__class_Ouminus("d1","d2") = "d0"
& c_HOL_Ouminus__class_Ouminus("d1","d1") = "d0"
& c_HOL_Ouminus__class_Ouminus("d1","d0") = "d1"
& c_HOL_Ouminus__class_Ouminus("d0","d2") = "d0"
& c_HOL_Ouminus__class_Ouminus("d0","d1") = "d0"
& c_HOL_Ouminus__class_Ouminus("d0","d0") = "d2"
& c_HOL_Osgn__class_Osgn("d2","d2") = "d0"
& c_HOL_Osgn__class_Osgn("d2","d1") = "d0"
& c_HOL_Osgn__class_Osgn("d2","d0") = "d2"
& c_HOL_Osgn__class_Osgn("d1","d2") = "d0"
& c_HOL_Osgn__class_Osgn("d1","d1") = "d0"
& c_HOL_Osgn__class_Osgn("d1","d0") = "d1"
& c_HOL_Osgn__class_Osgn("d0","d2") = "d0"
& c_HOL_Osgn__class_Osgn("d0","d1") = "d0"
& c_HOL_Osgn__class_Osgn("d0","d0") = "d0"
& c_HOL_Oinverse__class_Oinverse("d2","d2") = "d0"
& c_HOL_Oinverse__class_Oinverse("d2","d1") = "d0"
& c_HOL_Oinverse__class_Oinverse("d2","d0") = "d2"
& c_HOL_Oinverse__class_Oinverse("d1","d2") = "d0"
& c_HOL_Oinverse__class_Oinverse("d1","d1") = "d0"
& c_HOL_Oinverse__class_Oinverse("d1","d0") = "d1"
& c_HOL_Oinverse__class_Oinverse("d0","d2") = "d0"
& c_HOL_Oinverse__class_Oinverse("d0","d1") = "d0"
& c_HOL_Oinverse__class_Oinverse("d0","d0") = "d0"
& c_HOL_Oabs__class_Oabs("d2","d2") = "d0"
& c_HOL_Oabs__class_Oabs("d2","d1") = "d0"
& c_HOL_Oabs__class_Oabs("d2","d0") = "d0"
& c_HOL_Oabs__class_Oabs("d1","d2") = "d0"
& c_HOL_Oabs__class_Oabs("d1","d1") = "d0"
& c_HOL_Oabs__class_Oabs("d1","d0") = "d1"
& c_HOL_Oabs__class_Oabs("d0","d2") = "d0"
& c_HOL_Oabs__class_Oabs("d0","d1") = "d0"
& c_HOL_Oabs__class_Oabs("d0","d0") = "d0"
& c_Fun_Oid("d2","d2") = "d2"
& c_Fun_Oid("d2","d1") = "d2"
& c_Fun_Oid("d2","d0") = "d2"
& c_Fun_Oid("d1","d2") = "d1"
& c_Fun_Oid("d1","d1") = "d1"
& c_Fun_Oid("d1","d0") = "d1"
& c_Fun_Oid("d0","d2") = "d0"
& c_Fun_Oid("d0","d1") = "d0"
& c_Fun_Oid("d0","d0") = "d0"
& c_Transcendental_Osin("d2") = "d1"
& c_Transcendental_Osin("d1") = "d1"
& c_Transcendental_Osin("d0") = "d1"
& c_Transcendental_Ocos("d2") = "d0"
& c_Transcendental_Ocos("d1") = "d0"
& c_Transcendental_Ocos("d0") = "d0"
& c_NthRoot_Osqrt("d2") = "d2"
& c_NthRoot_Osqrt("d1") = "d1"
& c_NthRoot_Osqrt("d0") = "d0"
& c_HOL_Ozero__class_Ozero("d2") = "d0"
& c_HOL_Ozero__class_Ozero("d1") = "d0"
& c_HOL_Ozero__class_Ozero("d0") = "d1"
& c_HOL_Oone__class_Oone("d2") = "d0"
& c_HOL_Oone__class_Oone("d1") = "d0"
& c_HOL_Oone__class_Oone("d0") = "d0"
& v_x = "d0"
& tc_RealDef_Oreal = "d0"
& t_a = "d0"
& c_Transcendental_Opi = "d0" ) ).
fof(interp_relations,interpretation-mappings,
( ~ c_lessequals("d2","d2","d2")
& ~ c_lessequals("d2","d2","d1")
& c_lessequals("d2","d2","d0")
& ~ c_lessequals("d2","d1","d2")
& ~ c_lessequals("d2","d1","d1")
& c_lessequals("d2","d1","d0")
& ~ c_lessequals("d2","d0","d2")
& ~ c_lessequals("d2","d0","d1")
& c_lessequals("d2","d0","d0")
& ~ c_lessequals("d1","d2","d2")
& ~ c_lessequals("d1","d2","d1")
& ~ c_lessequals("d1","d2","d0")
& ~ c_lessequals("d1","d1","d2")
& ~ c_lessequals("d1","d1","d1")
& c_lessequals("d1","d1","d0")
& ~ c_lessequals("d1","d0","d2")
& ~ c_lessequals("d1","d0","d1")
& c_lessequals("d1","d0","d0")
& ~ c_lessequals("d0","d2","d2")
& ~ c_lessequals("d0","d2","d1")
& ~ c_lessequals("d0","d2","d0")
& ~ c_lessequals("d0","d1","d2")
& ~ c_lessequals("d0","d1","d1")
& ~ c_lessequals("d0","d1","d0")
& ~ c_lessequals("d0","d0","d2")
& ~ c_lessequals("d0","d0","d1")
& c_lessequals("d0","d0","d0")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d2","d2","d2")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d2","d2","d1")
& c_Ring__and__Field_Odvd__class_Odvd("d2","d2","d0")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d2","d1","d2")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d2","d1","d1")
& c_Ring__and__Field_Odvd__class_Odvd("d2","d1","d0")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d2","d0","d2")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d2","d0","d1")
& c_Ring__and__Field_Odvd__class_Odvd("d2","d0","d0")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d1","d2","d2")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d1","d2","d1")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d1","d2","d0")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d1","d1","d2")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d1","d1","d1")
& c_Ring__and__Field_Odvd__class_Odvd("d1","d1","d0")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d1","d0","d2")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d1","d0","d1")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d1","d0","d0")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d0","d2","d2")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d0","d2","d1")
& c_Ring__and__Field_Odvd__class_Odvd("d0","d2","d0")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d0","d1","d2")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d0","d1","d1")
& c_Ring__and__Field_Odvd__class_Odvd("d0","d1","d0")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d0","d0","d2")
& ~ c_Ring__and__Field_Odvd__class_Odvd("d0","d0","d1")
& c_Ring__and__Field_Odvd__class_Odvd("d0","d0","d0")
& ~ c_Int_Oiszero("d2","d2")
& ~ c_Int_Oiszero("d2","d1")
& ~ c_Int_Oiszero("d2","d0")
& ~ c_Int_Oiszero("d1","d2")
& ~ c_Int_Oiszero("d1","d1")
& c_Int_Oiszero("d1","d0")
& ~ c_Int_Oiszero("d0","d2")
& ~ c_Int_Oiszero("d0","d1")
& ~ c_Int_Oiszero("d0","d0")
& ~ class_Ring__and__Field_Ozero__neq__one("d2")
& ~ class_Ring__and__Field_Ozero__neq__one("d1")
& class_Ring__and__Field_Ozero__neq__one("d0")
& ~ class_Ring__and__Field_Osgn__if("d2")
& ~ class_Ring__and__Field_Osgn__if("d1")
& class_Ring__and__Field_Osgn__if("d0")
& ~ class_Ring__and__Field_Osemiring__1("d2")
& ~ class_Ring__and__Field_Osemiring__1("d1")
& class_Ring__and__Field_Osemiring__1("d0")
& ~ class_Ring__and__Field_Oring__no__zero__divisors("d2")
& ~ class_Ring__and__Field_Oring__no__zero__divisors("d1")
& class_Ring__and__Field_Oring__no__zero__divisors("d0")
& ~ class_Ring__and__Field_Oring__1__no__zero__divisors("d2")
& ~ class_Ring__and__Field_Oring__1__no__zero__divisors("d1")
& class_Ring__and__Field_Oring__1__no__zero__divisors("d0")
& ~ class_Ring__and__Field_Oring__1("d2")
& ~ class_Ring__and__Field_Oring__1("d1")
& class_Ring__and__Field_Oring__1("d0")
& ~ class_Ring__and__Field_Oring("d2")
& ~ class_Ring__and__Field_Oring("d1")
& class_Ring__and__Field_Oring("d0")
& ~ class_Ring__and__Field_Opordered__semiring("d2")
& ~ class_Ring__and__Field_Opordered__semiring("d1")
& class_Ring__and__Field_Opordered__semiring("d0")
& ~ class_Ring__and__Field_Opordered__ring__abs("d2")
& ~ class_Ring__and__Field_Opordered__ring__abs("d1")
& class_Ring__and__Field_Opordered__ring__abs("d0")
& ~ class_Ring__and__Field_Opordered__ring("d2")
& ~ class_Ring__and__Field_Opordered__ring("d1")
& class_Ring__and__Field_Opordered__ring("d0")
& ~ class_Ring__and__Field_Opordered__cancel__semiring("d2")
& ~ class_Ring__and__Field_Opordered__cancel__semiring("d1")
& class_Ring__and__Field_Opordered__cancel__semiring("d0")
& ~ class_Ring__and__Field_Oordered__semidom("d2")
& ~ class_Ring__and__Field_Oordered__semidom("d1")
& class_Ring__and__Field_Oordered__semidom("d0")
& ~ class_Ring__and__Field_Oordered__ring__strict("d2")
& ~ class_Ring__and__Field_Oordered__ring__strict("d1")
& class_Ring__and__Field_Oordered__ring__strict("d0")
& ~ class_Ring__and__Field_Oordered__idom("d2")
& ~ class_Ring__and__Field_Oordered__idom("d1")
& class_Ring__and__Field_Oordered__idom("d0")
& ~ class_Ring__and__Field_Oordered__field("d2")
& ~ class_Ring__and__Field_Oordered__field("d1")
& class_Ring__and__Field_Oordered__field("d0")
& ~ class_Ring__and__Field_Ono__zero__divisors("d2")
& ~ class_Ring__and__Field_Ono__zero__divisors("d1")
& class_Ring__and__Field_Ono__zero__divisors("d0")
& ~ class_Ring__and__Field_Omult__zero("d2")
& ~ class_Ring__and__Field_Omult__zero("d1")
& class_Ring__and__Field_Omult__zero("d0")
& ~ class_Ring__and__Field_Omult__mono1("d2")
& ~ class_Ring__and__Field_Omult__mono1("d1")
& class_Ring__and__Field_Omult__mono1("d0")
& ~ class_Ring__and__Field_Omult__mono("d2")
& ~ class_Ring__and__Field_Omult__mono("d1")
& class_Ring__and__Field_Omult__mono("d0")
& ~ class_Ring__and__Field_Olordered__ring("d2")
& ~ class_Ring__and__Field_Olordered__ring("d1")
& class_Ring__and__Field_Olordered__ring("d0")
& ~ class_Ring__and__Field_Oidom("d2")
& ~ class_Ring__and__Field_Oidom("d1")
& class_Ring__and__Field_Oidom("d0")
& ~ class_Ring__and__Field_Ofield("d2")
& ~ class_Ring__and__Field_Ofield("d1")
& class_Ring__and__Field_Ofield("d0")
& ~ class_Ring__and__Field_Odvd("d2")
& ~ class_Ring__and__Field_Odvd("d1")
& class_Ring__and__Field_Odvd("d0")
& ~ class_Ring__and__Field_Odivision__ring("d2")
& ~ class_Ring__and__Field_Odivision__ring("d1")
& class_Ring__and__Field_Odivision__ring("d0")
& ~ class_Ring__and__Field_Odivision__by__zero("d2")
& ~ class_Ring__and__Field_Odivision__by__zero("d1")
& class_Ring__and__Field_Odivision__by__zero("d0")
& ~ class_Ring__and__Field_Ocomm__semiring__1("d2")
& ~ class_Ring__and__Field_Ocomm__semiring__1("d1")
& class_Ring__and__Field_Ocomm__semiring__1("d0")
& ~ class_Ring__and__Field_Ocomm__ring__1("d2")
& ~ class_Ring__and__Field_Ocomm__ring__1("d1")
& class_Ring__and__Field_Ocomm__ring__1("d0")
& ~ class_RealVector_Oreal__vector("d2")
& ~ class_RealVector_Oreal__vector("d1")
& class_RealVector_Oreal__vector("d0")
& ~ class_RealVector_Oreal__normed__vector("d2")
& ~ class_RealVector_Oreal__normed__vector("d1")
& class_RealVector_Oreal__normed__vector("d0")
& ~ class_RealVector_Oreal__normed__field("d2")
& ~ class_RealVector_Oreal__normed__field("d1")
& class_RealVector_Oreal__normed__field("d0")
& ~ class_RealVector_Oreal__normed__div__algebra("d2")
& ~ class_RealVector_Oreal__normed__div__algebra("d1")
& class_RealVector_Oreal__normed__div__algebra("d0")
& ~ class_RealVector_Oreal__normed__algebra__1("d2")
& ~ class_RealVector_Oreal__normed__algebra__1("d1")
& class_RealVector_Oreal__normed__algebra__1("d0")
& ~ class_RealVector_Oreal__normed__algebra("d2")
& ~ class_RealVector_Oreal__normed__algebra("d1")
& class_RealVector_Oreal__normed__algebra("d0")
& ~ class_RealVector_Oreal__algebra__1("d2")
& ~ class_RealVector_Oreal__algebra__1("d1")
& class_RealVector_Oreal__algebra__1("d0")
& ~ class_RealVector_Oreal__algebra("d2")
& ~ class_RealVector_Oreal__algebra("d1")
& class_RealVector_Oreal__algebra("d0")
& ~ class_Power_Opower("d2")
& ~ class_Power_Opower("d1")
& class_Power_Opower("d0")
& ~ class_Orderings_Opreorder("d2")
& ~ class_Orderings_Opreorder("d1")
& class_Orderings_Opreorder("d0")
& ~ class_Orderings_Oorder("d2")
& ~ class_Orderings_Oorder("d1")
& class_Orderings_Oorder("d0")
& ~ class_Orderings_Olinorder("d2")
& ~ class_Orderings_Olinorder("d1")
& class_Orderings_Olinorder("d0")
& ~ class_OrderedGroup_Opordered__ab__group__add__abs("d2")
& ~ class_OrderedGroup_Opordered__ab__group__add__abs("d1")
& class_OrderedGroup_Opordered__ab__group__add__abs("d0")
& ~ class_OrderedGroup_Opordered__ab__group__add("d2")
& ~ class_OrderedGroup_Opordered__ab__group__add("d1")
& class_OrderedGroup_Opordered__ab__group__add("d0")
& ~ class_OrderedGroup_Oordered__ab__group__add("d2")
& ~ class_OrderedGroup_Oordered__ab__group__add("d1")
& class_OrderedGroup_Oordered__ab__group__add("d0")
& ~ class_OrderedGroup_Omonoid__mult("d2")
& ~ class_OrderedGroup_Omonoid__mult("d1")
& class_OrderedGroup_Omonoid__mult("d0")
& ~ class_OrderedGroup_Olordered__ab__group__add("d2")
& ~ class_OrderedGroup_Olordered__ab__group__add("d1")
& class_OrderedGroup_Olordered__ab__group__add("d0")
& ~ class_OrderedGroup_Ogroup__add("d2")
& ~ class_OrderedGroup_Ogroup__add("d1")
& class_OrderedGroup_Ogroup__add("d0")
& ~ class_OrderedGroup_Ocomm__monoid__mult("d2")
& ~ class_OrderedGroup_Ocomm__monoid__mult("d1")
& class_OrderedGroup_Ocomm__monoid__mult("d0")
& ~ class_OrderedGroup_Oab__semigroup__mult("d2")
& ~ class_OrderedGroup_Oab__semigroup__mult("d1")
& class_OrderedGroup_Oab__semigroup__mult("d0")
& ~ class_OrderedGroup_Oab__semigroup__idem__mult("d2")
& ~ class_OrderedGroup_Oab__semigroup__idem__mult("d1")
& ~ class_OrderedGroup_Oab__semigroup__idem__mult("d0")
& ~ class_Lattices_Oboolean__algebra("d2")
& ~ class_Lattices_Oboolean__algebra("d1")
& ~ class_Lattices_Oboolean__algebra("d0")
& ~ class_Int_Onumber__ring("d2")
& ~ class_Int_Onumber__ring("d1")
& class_Int_Onumber__ring("d0")
& ~ class_Divides_Osemiring__div("d2")
& ~ class_Divides_Osemiring__div("d1")
& ~ class_Divides_Osemiring__div("d0")
& ~ class_Divides_Oring__div("d2")
& ~ class_Divides_Oring__div("d1")
& ~ class_Divides_Oring__div("d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV595-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : mace4 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/5.38 % Computer : n026.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Sat Sep 26 14:38:01 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.39 % Mace4 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/5.39 % Process 1246166 was started by sandbox on n026,
% 0.10/5.39 % Sat Sep 26 14:38:01 2026
% 0.10/5.39 % The command was "/export/starexec/sandbox/solver/bin/mace4 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/5.55
% 0.14/5.55 % SZS status Satisfiable for theBenchmark
% 0.14/5.55 % SZS output start FiniteModel for theBenchmark
% See solution above
%------------------------------------------------------------------------------