%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : SWB036+1 : TPTP v9.2.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n011.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 : 300s % DateTime : Wed Jun 3 08:57:34 AM UTC 2026 % Result : Satisfiable 38.03s 38.28s % Output : Model 38.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWB036+1 : TPTP v9.2.1. Released v5.2.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.17/0.34 % Computer : n011.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Tue Jun 2 18:58:19 EDT 2026 % 0.17/0.34 % CPUTime : % 0.38/0.61 %----Disproving FOF, CNF % 0.46/0.62 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 12... % 12.72/13.00 --- Run --no-e-matching --full-saturate-quant at 12... % 24.86/25.12 --- Run --no-e-matching --enum-inst-sum --full-saturate-quant at 12... % 37.02/37.24 --- Run --finite-model-find --uf-ss=no-minimal at 54... % 38.03/38.28 % SZS status Satisfiable % 38.03/38.28 % SZS output start Model % 38.03/38.28 ( % 38.03/38.28 ; cardinality of $$unsorted is 7 % 38.03/38.28 ; rep: (as @$$unsorted_0 $$unsorted) % 38.03/38.28 ; rep: (as @$$unsorted_1 $$unsorted) % 38.03/38.28 ; rep: (as @$$unsorted_2 $$unsorted) % 38.03/38.28 ; rep: (as @$$unsorted_3 $$unsorted) % 38.03/38.28 ; rep: (as @$$unsorted_4 $$unsorted) % 38.03/38.28 ; rep: (as @$$unsorted_5 $$unsorted) % 38.03/38.28 ; rep: (as @$$unsorted_6 $$unsorted) % 38.03/38.28 (define-fun tptp.abstractDomain (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x1))) % 38.03/38.28 (define-fun tptp.dataDomain (($x1 $$unsorted)) Bool (= (as @$$unsorted_5 $$unsorted) $x1)) % 38.03/38.28 (define-fun tptp.iowlThing (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x1))) % 38.03/38.28 (define-fun tptp.iowlNothing (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.xsd_string (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.xsd_integer (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iAmerican (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.ihasTopping (($x1 $$unsorted) ($x2 $$unsorted)) Bool (or (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x2)))) % 38.03/38.28 (define-fun tptp.iMozzarellaTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iNamedPizza (($x1 $$unsorted)) Bool (and (not (= (as @$$unsorted_5 $$unsorted) $x1)) (not (= (as @$$unsorted_6 $$unsorted) $x1)) (not (= (as @$$unsorted_1 $$unsorted) $x1)) (not (= (as @$$unsorted_2 $$unsorted) $x1)) (not (= (as @$$unsorted_3 $$unsorted) $x1)) (not (= (as @$$unsorted_4 $$unsorted) $x1)))) % 38.03/38.28 (define-fun tptp.iPeperoniSausageTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iTomatoTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iAmerica () $$unsorted (as @$$unsorted_0 $$unsorted)) % 38.03/38.28 (define-fun tptp.ihasCountryOfOrigin (($x1 $$unsorted) ($x2 $$unsorted)) Bool (and (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x2))) (not (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2))))) % 38.03/38.28 (define-fun tptp.iAmericanHot (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iJalapenoPepperTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iHotGreenPepperTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iAnchoviesTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iFishTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iArtichokeTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.ihasSpiciness (($x1 $$unsorted) ($x2 $$unsorted)) Bool (or (and (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2)) (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2)) (and (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2)))) % 38.03/38.28 (define-fun tptp.iMild (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iVegetableTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iAsparagusTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iCajun (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iPeperonataTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iTobascoPepperSauce (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iOnionTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iPrawnsTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iCajunSpiceTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iHerbSpiceTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iHot (($x1 $$unsorted)) Bool (= (as @$$unsorted_6 $$unsorted) $x1)) % 38.03/38.28 (define-fun tptp.iCaperTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iCapricciosa (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iHamTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iOliveTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iCaprina (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iSundriedTomatoTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iGoatsCheeseTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iCheeseTopping (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1))) % 38.03/38.28 (define-fun tptp.iPizzaTopping (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1))) % 38.03/38.28 (define-fun tptp.iCheeseyPizza (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 38.03/38.28 (define-fun tptp.iPizza (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 38.03/38.28 (define-fun tptp.iCheeseyVegetableTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iChickenTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iMeatTopping (($x1 $$unsorted)) Bool (= (as @$$unsorted_2 $$unsorted) $x1)) % 38.03/38.28 (define-fun tptp.iCountry (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 38.03/38.28 (define-fun tptp.iDomainConcept (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 38.03/38.28 (define-fun tptp.iFrance () $$unsorted (as @$$unsorted_2 $$unsorted)) % 38.03/38.28 (define-fun tptp.iItaly () $$unsorted (as @$$unsorted_4 $$unsorted)) % 38.03/38.28 (define-fun tptp.iGermany () $$unsorted (as @$$unsorted_3 $$unsorted)) % 38.03/38.28 (define-fun tptp.iEngland () $$unsorted (as @$$unsorted_1 $$unsorted)) % 38.03/38.28 (define-fun tptp.iDeepPanBase (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iPizzaBase (($x1 $$unsorted)) Bool (= (as @$$unsorted_4 $$unsorted) $x1)) % 38.03/38.28 (define-fun tptp.iFiorentina (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iParmesanTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iGarlicTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iSpinachTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iFood (($x1 $$unsorted)) Bool (and (not (= (as @$$unsorted_5 $$unsorted) $x1)) (not (= (as @$$unsorted_6 $$unsorted) $x1)))) % 38.03/38.28 (define-fun tptp.iFourCheesesTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iFourSeasons (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iMushroomTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iFruitTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iFruttiDiMare (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iMixedSeafoodTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iMedium (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iGiardiniera (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iPetitPoisTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iSlicedTomatoTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iLeekTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iGorgonzolaTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iGreenPepperTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iPepperTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iSpiciness (($x1 $$unsorted)) Bool (= (as @$$unsorted_6 $$unsorted) $x1)) % 38.03/38.28 (define-fun tptp.iHotSpicedBeefTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iIceCream (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iInterestingPizza (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 38.03/38.28 (define-fun tptp.iLaReine (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iMargherita (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iMeatyPizza (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 38.03/38.28 (define-fun tptp.iMushroom (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iNapoletana (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iNonVegetarianPizza (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 38.03/38.28 (define-fun tptp.iVegetarianPizza (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iNutTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iParmaHamTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iParmense (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iPineKernels (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.ihasBase (($x1 $$unsorted) ($x2 $$unsorted)) Bool (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2))) % 38.03/38.28 (define-fun tptp.iPolloAdAstra (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iSweetPepperTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iRedOnionTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iPrinceCarlo (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iRosemaryTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iQuattroFormaggi (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iRealItalianPizza (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iThinAndCrispyBase (($x1 $$unsorted)) Bool (= (as @$$unsorted_4 $$unsorted) $x1)) % 38.03/38.28 (define-fun tptp.iRocketTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iRosa (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iSauceTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iSiciliana (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iSloppyGiuseppe (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iSoho (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iValuePartition (($x1 $$unsorted)) Bool (= (as @$$unsorted_6 $$unsorted) $x1)) % 38.03/38.28 (define-fun tptp.iSpicyPizza (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 38.03/38.28 (define-fun tptp.iSpicyTopping (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1))) % 38.03/38.28 (define-fun tptp.iSpicyPizzaEquivalent (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 38.03/38.28 (define-fun tptp.iSultanaTopping (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iThinAndCrispyPizza (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 38.03/38.28 (define-fun tptp.iUnclosedPizza (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iVegetarianPizzaEquivalent1 (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iVegetarianTopping (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1))) % 38.03/38.28 (define-fun tptp.iVegetarianPizzaEquivalent2 (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iVeneziana (($x1 $$unsorted)) Bool false) % 38.03/38.28 (define-fun tptp.iisBaseOf (($x1 $$unsorted) ($x2 $$unsorted)) Bool (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2))) % 38.03/38.28 (define-fun tptp.ihasIngredient (($x1 $$unsorted) ($x2 $$unsorted)) Bool (and (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x2))) (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2))) (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2))) (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))))) % 38.03/38.28 (define-fun tptp.iisIngredientOf (($x1 $$unsorted) ($x2 $$unsorted)) Bool (and (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x2))) (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2))) (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2))) (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))))) % 38.03/38.28 (define-fun tptp.iisToppingOf (($x1 $$unsorted) ($x2 $$unsorted)) Bool (or (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2)) (and (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2)) (and (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2)))) % 38.03/38.28 ) % 38.03/38.28 % SZS output end Model % 38.03/38.28 % cvc5 exiting %------------------------------------------------------------------------------