%------------------------------------------------------------------------------
% File : Mace4---2026-6A
% Problem : SWB036+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : mace4 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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 08:51:19 AM UTC 2026
% Result : Satisfiable 0.14s 10.63s
% Output : FiniteModel 0.14s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(interp_domain,interpretation-domains,
! [X] :
( X = "d5"
| X = "d4"
| X = "d3"
| X = "d2"
| X = "d1"
| X = "d0" ) ).
fof(interp_functions,interpretation-mappings,
( iItaly = "d5"
& iGermany = "d4"
& iFrance = "d3"
& iEngland = "d2"
& iAmerica = "d0"
& f161("d5") = "d0"
& f161("d4") = "d0"
& f161("d3") = "d0"
& f161("d2") = "d0"
& f161("d1") = "d0"
& f161("d0") = "d0"
& f160("d5") = "d0"
& f160("d4") = "d0"
& f160("d3") = "d0"
& f160("d2") = "d0"
& f160("d1") = "d0"
& f160("d0") = "d0"
& f159("d5") = "d0"
& f159("d4") = "d0"
& f159("d3") = "d0"
& f159("d2") = "d0"
& f159("d1") = "d0"
& f159("d0") = "d0"
& f158("d5") = "d0"
& f158("d4") = "d0"
& f158("d3") = "d0"
& f158("d2") = "d0"
& f158("d1") = "d0"
& f158("d0") = "d0"
& f157("d5") = "d0"
& f157("d4") = "d0"
& f157("d3") = "d0"
& f157("d2") = "d0"
& f157("d1") = "d0"
& f157("d0") = "d0"
& f156("d5") = "d0"
& f156("d4") = "d0"
& f156("d3") = "d0"
& f156("d2") = "d0"
& f156("d1") = "d0"
& f156("d0") = "d0"
& f155("d5") = "d0"
& f155("d4") = "d0"
& f155("d3") = "d0"
& f155("d2") = "d0"
& f155("d1") = "d0"
& f155("d0") = "d0"
& f154("d5") = "d0"
& f154("d4") = "d0"
& f154("d3") = "d0"
& f154("d2") = "d0"
& f154("d1") = "d0"
& f154("d0") = "d0"
& f153("d5") = "d0"
& f153("d4") = "d0"
& f153("d3") = "d0"
& f153("d2") = "d0"
& f153("d1") = "d0"
& f153("d0") = "d0"
& f152("d5") = "d0"
& f152("d4") = "d0"
& f152("d3") = "d0"
& f152("d2") = "d0"
& f152("d1") = "d0"
& f152("d0") = "d0"
& f151("d5") = "d0"
& f151("d4") = "d0"
& f151("d3") = "d0"
& f151("d2") = "d0"
& f151("d1") = "d0"
& f151("d0") = "d0"
& f150("d5") = "d0"
& f150("d4") = "d0"
& f150("d3") = "d0"
& f150("d2") = "d0"
& f150("d1") = "d0"
& f150("d0") = "d0"
& f149("d5") = "d0"
& f149("d4") = "d0"
& f149("d3") = "d0"
& f149("d2") = "d0"
& f149("d1") = "d0"
& f149("d0") = "d0"
& f148("d5") = "d0"
& f148("d4") = "d0"
& f148("d3") = "d0"
& f148("d2") = "d0"
& f148("d1") = "d0"
& f148("d0") = "d0"
& f147("d5") = "d0"
& f147("d4") = "d0"
& f147("d3") = "d0"
& f147("d2") = "d0"
& f147("d1") = "d0"
& f147("d0") = "d0"
& f146("d5") = "d0"
& f146("d4") = "d0"
& f146("d3") = "d0"
& f146("d2") = "d0"
& f146("d1") = "d0"
& f146("d0") = "d0"
& f145("d5") = "d0"
& f145("d4") = "d0"
& f145("d3") = "d0"
& f145("d2") = "d0"
& f145("d1") = "d0"
& f145("d0") = "d0"
& f144("d5") = "d0"
& f144("d4") = "d0"
& f144("d3") = "d0"
& f144("d2") = "d0"
& f144("d1") = "d0"
& f144("d0") = "d0"
& f143("d5") = "d0"
& f143("d4") = "d0"
& f143("d3") = "d0"
& f143("d2") = "d0"
& f143("d1") = "d0"
& f143("d0") = "d0"
& f142("d5") = "d0"
& f142("d4") = "d0"
& f142("d3") = "d0"
& f142("d2") = "d0"
& f142("d1") = "d0"
& f142("d0") = "d0"
& f141("d5") = "d0"
& f141("d4") = "d0"
& f141("d3") = "d0"
& f141("d2") = "d0"
& f141("d1") = "d0"
& f141("d0") = "d0"
& f140("d5") = "d0"
& f140("d4") = "d0"
& f140("d3") = "d0"
& f140("d2") = "d0"
& f140("d1") = "d0"
& f140("d0") = "d0"
& f139("d5") = "d0"
& f139("d4") = "d0"
& f139("d3") = "d0"
& f139("d2") = "d0"
& f139("d1") = "d0"
& f139("d0") = "d0"
& f138("d5") = "d0"
& f138("d4") = "d0"
& f138("d3") = "d0"
& f138("d2") = "d0"
& f138("d1") = "d0"
& f138("d0") = "d0"
& f137("d5") = "d0"
& f137("d4") = "d0"
& f137("d3") = "d0"
& f137("d2") = "d0"
& f137("d1") = "d0"
& f137("d0") = "d0"
& f136("d5") = "d0"
& f136("d4") = "d0"
& f136("d3") = "d0"
& f136("d2") = "d0"
& f136("d1") = "d0"
& f136("d0") = "d0"
& f135("d5") = "d0"
& f135("d4") = "d0"
& f135("d3") = "d0"
& f135("d2") = "d0"
& f135("d1") = "d0"
& f135("d0") = "d0"
& f134("d5") = "d0"
& f134("d4") = "d0"
& f134("d3") = "d0"
& f134("d2") = "d0"
& f134("d1") = "d0"
& f134("d0") = "d0"
& f133("d5") = "d0"
& f133("d4") = "d0"
& f133("d3") = "d0"
& f133("d2") = "d0"
& f133("d1") = "d0"
& f133("d0") = "d0"
& f132("d5") = "d0"
& f132("d4") = "d0"
& f132("d3") = "d0"
& f132("d2") = "d0"
& f132("d1") = "d0"
& f132("d0") = "d0"
& f131("d5") = "d0"
& f131("d4") = "d0"
& f131("d3") = "d0"
& f131("d2") = "d0"
& f131("d1") = "d0"
& f131("d0") = "d0"
& f130("d5") = "d0"
& f130("d4") = "d0"
& f130("d3") = "d0"
& f130("d2") = "d0"
& f130("d1") = "d0"
& f130("d0") = "d0"
& f129("d5") = "d0"
& f129("d4") = "d0"
& f129("d3") = "d0"
& f129("d2") = "d0"
& f129("d1") = "d0"
& f129("d0") = "d0"
& f128("d5") = "d0"
& f128("d4") = "d0"
& f128("d3") = "d0"
& f128("d2") = "d0"
& f128("d1") = "d0"
& f128("d0") = "d0"
& f127("d5") = "d0"
& f127("d4") = "d0"
& f127("d3") = "d0"
& f127("d2") = "d0"
& f127("d1") = "d0"
& f127("d0") = "d0"
& f126("d5") = "d0"
& f126("d4") = "d0"
& f126("d3") = "d0"
& f126("d2") = "d0"
& f126("d1") = "d0"
& f126("d0") = "d0"
& f125("d5") = "d0"
& f125("d4") = "d0"
& f125("d3") = "d0"
& f125("d2") = "d0"
& f125("d1") = "d0"
& f125("d0") = "d0"
& f124("d5") = "d0"
& f124("d4") = "d0"
& f124("d3") = "d0"
& f124("d2") = "d0"
& f124("d1") = "d0"
& f124("d0") = "d0"
& f123("d5") = "d0"
& f123("d4") = "d0"
& f123("d3") = "d0"
& f123("d2") = "d0"
& f123("d1") = "d0"
& f123("d0") = "d0"
& f122("d5") = "d0"
& f122("d4") = "d0"
& f122("d3") = "d0"
& f122("d2") = "d0"
& f122("d1") = "d0"
& f122("d0") = "d0"
& f121("d5") = "d0"
& f121("d4") = "d0"
& f121("d3") = "d0"
& f121("d2") = "d0"
& f121("d1") = "d0"
& f121("d0") = "d0"
& f120("d5") = "d0"
& f120("d4") = "d0"
& f120("d3") = "d0"
& f120("d2") = "d0"
& f120("d1") = "d0"
& f120("d0") = "d0"
& f119("d5") = "d0"
& f119("d4") = "d0"
& f119("d3") = "d0"
& f119("d2") = "d0"
& f119("d1") = "d0"
& f119("d0") = "d0"
& f118("d5") = "d0"
& f118("d4") = "d0"
& f118("d3") = "d0"
& f118("d2") = "d0"
& f118("d1") = "d0"
& f118("d0") = "d0"
& f117("d5") = "d0"
& f117("d4") = "d0"
& f117("d3") = "d0"
& f117("d2") = "d0"
& f117("d1") = "d0"
& f117("d0") = "d0"
& f116("d5") = "d0"
& f116("d4") = "d0"
& f116("d3") = "d0"
& f116("d2") = "d0"
& f116("d1") = "d0"
& f116("d0") = "d0"
& f115("d5") = "d0"
& f115("d4") = "d0"
& f115("d3") = "d0"
& f115("d2") = "d0"
& f115("d1") = "d0"
& f115("d0") = "d0"
& f114("d5") = "d0"
& f114("d4") = "d0"
& f114("d3") = "d0"
& f114("d2") = "d0"
& f114("d1") = "d0"
& f114("d0") = "d0"
& f113("d5") = "d0"
& f113("d4") = "d0"
& f113("d3") = "d0"
& f113("d2") = "d0"
& f113("d1") = "d0"
& f113("d0") = "d0"
& f112("d5") = "d0"
& f112("d4") = "d0"
& f112("d3") = "d0"
& f112("d2") = "d0"
& f112("d1") = "d0"
& f112("d0") = "d0"
& f111("d5") = "d0"
& f111("d4") = "d0"
& f111("d3") = "d0"
& f111("d2") = "d0"
& f111("d1") = "d0"
& f111("d0") = "d0"
& f110("d5") = "d0"
& f110("d4") = "d0"
& f110("d3") = "d0"
& f110("d2") = "d0"
& f110("d1") = "d0"
& f110("d0") = "d0"
& f109("d5") = "d0"
& f109("d4") = "d0"
& f109("d3") = "d0"
& f109("d2") = "d0"
& f109("d1") = "d0"
& f109("d0") = "d0"
& f108("d5") = "d0"
& f108("d4") = "d0"
& f108("d3") = "d0"
& f108("d2") = "d0"
& f108("d1") = "d0"
& f108("d0") = "d0"
& f107("d5") = "d0"
& f107("d4") = "d0"
& f107("d3") = "d0"
& f107("d2") = "d0"
& f107("d1") = "d0"
& f107("d0") = "d0"
& f106("d5") = "d0"
& f106("d4") = "d0"
& f106("d3") = "d0"
& f106("d2") = "d0"
& f106("d1") = "d0"
& f106("d0") = "d0"
& f105("d5") = "d0"
& f105("d4") = "d0"
& f105("d3") = "d0"
& f105("d2") = "d0"
& f105("d1") = "d0"
& f105("d0") = "d0"
& f104("d5") = "d0"
& f104("d4") = "d0"
& f104("d3") = "d0"
& f104("d2") = "d0"
& f104("d1") = "d0"
& f104("d0") = "d0"
& f103("d5") = "d0"
& f103("d4") = "d0"
& f103("d3") = "d0"
& f103("d2") = "d0"
& f103("d1") = "d0"
& f103("d0") = "d0"
& f102("d5") = "d0"
& f102("d4") = "d0"
& f102("d3") = "d0"
& f102("d2") = "d0"
& f102("d1") = "d0"
& f102("d0") = "d0"
& f101("d5") = "d0"
& f101("d4") = "d0"
& f101("d3") = "d0"
& f101("d2") = "d0"
& f101("d1") = "d0"
& f101("d0") = "d0"
& f100("d5") = "d0"
& f100("d4") = "d0"
& f100("d3") = "d0"
& f100("d2") = "d0"
& f100("d1") = "d0"
& f100("d0") = "d0"
& f99("d5") = "d0"
& f99("d4") = "d0"
& f99("d3") = "d0"
& f99("d2") = "d0"
& f99("d1") = "d0"
& f99("d0") = "d0"
& f98("d5") = "d0"
& f98("d4") = "d0"
& f98("d3") = "d0"
& f98("d2") = "d0"
& f98("d1") = "d0"
& f98("d0") = "d0"
& f97("d5") = "d0"
& f97("d4") = "d0"
& f97("d3") = "d0"
& f97("d2") = "d0"
& f97("d1") = "d0"
& f97("d0") = "d0"
& f96("d5") = "d0"
& f96("d4") = "d0"
& f96("d3") = "d0"
& f96("d2") = "d0"
& f96("d1") = "d0"
& f96("d0") = "d0"
& f95("d5") = "d0"
& f95("d4") = "d0"
& f95("d3") = "d0"
& f95("d2") = "d0"
& f95("d1") = "d0"
& f95("d0") = "d0"
& f94("d5") = "d0"
& f94("d4") = "d0"
& f94("d3") = "d0"
& f94("d2") = "d0"
& f94("d1") = "d0"
& f94("d0") = "d0"
& f93("d5") = "d0"
& f93("d4") = "d0"
& f93("d3") = "d0"
& f93("d2") = "d0"
& f93("d1") = "d0"
& f93("d0") = "d0"
& f92("d5") = "d0"
& f92("d4") = "d0"
& f92("d3") = "d0"
& f92("d2") = "d0"
& f92("d1") = "d0"
& f92("d0") = "d0"
& f91("d5") = "d0"
& f91("d4") = "d0"
& f91("d3") = "d0"
& f91("d2") = "d0"
& f91("d1") = "d0"
& f91("d0") = "d0"
& f90("d5") = "d0"
& f90("d4") = "d0"
& f90("d3") = "d0"
& f90("d2") = "d0"
& f90("d1") = "d0"
& f90("d0") = "d0"
& f89("d5") = "d0"
& f89("d4") = "d0"
& f89("d3") = "d0"
& f89("d2") = "d0"
& f89("d1") = "d0"
& f89("d0") = "d0"
& f88("d5") = "d0"
& f88("d4") = "d0"
& f88("d3") = "d0"
& f88("d2") = "d0"
& f88("d1") = "d0"
& f88("d0") = "d0"
& f87("d5") = "d0"
& f87("d4") = "d0"
& f87("d3") = "d0"
& f87("d2") = "d0"
& f87("d1") = "d0"
& f87("d0") = "d0"
& f86("d5") = "d0"
& f86("d4") = "d0"
& f86("d3") = "d0"
& f86("d2") = "d0"
& f86("d1") = "d0"
& f86("d0") = "d0"
& f85("d5") = "d0"
& f85("d4") = "d0"
& f85("d3") = "d0"
& f85("d2") = "d0"
& f85("d1") = "d0"
& f85("d0") = "d0"
& f84("d5") = "d0"
& f84("d4") = "d0"
& f84("d3") = "d0"
& f84("d2") = "d0"
& f84("d1") = "d0"
& f84("d0") = "d0"
& f83("d5") = "d0"
& f83("d4") = "d0"
& f83("d3") = "d0"
& f83("d2") = "d0"
& f83("d1") = "d0"
& f83("d0") = "d0"
& f82("d5") = "d0"
& f82("d4") = "d0"
& f82("d3") = "d0"
& f82("d2") = "d0"
& f82("d1") = "d0"
& f82("d0") = "d0"
& f81("d5") = "d0"
& f81("d4") = "d0"
& f81("d3") = "d0"
& f81("d2") = "d0"
& f81("d1") = "d0"
& f81("d0") = "d0"
& f80("d5") = "d0"
& f80("d4") = "d0"
& f80("d3") = "d0"
& f80("d2") = "d0"
& f80("d1") = "d0"
& f80("d0") = "d0"
& f79("d5") = "d0"
& f79("d4") = "d0"
& f79("d3") = "d0"
& f79("d2") = "d0"
& f79("d1") = "d0"
& f79("d0") = "d0"
& f78("d5") = "d0"
& f78("d4") = "d0"
& f78("d3") = "d0"
& f78("d2") = "d0"
& f78("d1") = "d0"
& f78("d0") = "d0"
& f77("d5") = "d0"
& f77("d4") = "d0"
& f77("d3") = "d0"
& f77("d2") = "d0"
& f77("d1") = "d0"
& f77("d0") = "d0"
& f76("d5") = "d0"
& f76("d4") = "d0"
& f76("d3") = "d0"
& f76("d2") = "d0"
& f76("d1") = "d0"
& f76("d0") = "d0"
& f75("d5") = "d0"
& f75("d4") = "d0"
& f75("d3") = "d0"
& f75("d2") = "d0"
& f75("d1") = "d0"
& f75("d0") = "d0"
& f74("d5") = "d0"
& f74("d4") = "d0"
& f74("d3") = "d0"
& f74("d2") = "d0"
& f74("d1") = "d0"
& f74("d0") = "d0"
& f73("d5") = "d0"
& f73("d4") = "d0"
& f73("d3") = "d0"
& f73("d2") = "d0"
& f73("d1") = "d0"
& f73("d0") = "d0"
& f72("d5") = "d0"
& f72("d4") = "d0"
& f72("d3") = "d0"
& f72("d2") = "d0"
& f72("d1") = "d0"
& f72("d0") = "d0"
& f71("d5") = "d0"
& f71("d4") = "d0"
& f71("d3") = "d0"
& f71("d2") = "d0"
& f71("d1") = "d0"
& f71("d0") = "d0"
& f70("d5") = "d0"
& f70("d4") = "d0"
& f70("d3") = "d0"
& f70("d2") = "d0"
& f70("d1") = "d0"
& f70("d0") = "d0"
& f69("d5") = "d0"
& f69("d4") = "d0"
& f69("d3") = "d0"
& f69("d2") = "d0"
& f69("d1") = "d0"
& f69("d0") = "d0"
& f68("d5") = "d0"
& f68("d4") = "d0"
& f68("d3") = "d0"
& f68("d2") = "d0"
& f68("d1") = "d0"
& f68("d0") = "d0"
& f67("d5") = "d0"
& f67("d4") = "d0"
& f67("d3") = "d0"
& f67("d2") = "d0"
& f67("d1") = "d0"
& f67("d0") = "d0"
& f66("d5") = "d0"
& f66("d4") = "d0"
& f66("d3") = "d0"
& f66("d2") = "d0"
& f66("d1") = "d0"
& f66("d0") = "d0"
& f65("d5") = "d0"
& f65("d4") = "d0"
& f65("d3") = "d0"
& f65("d2") = "d0"
& f65("d1") = "d0"
& f65("d0") = "d0"
& f64("d5") = "d0"
& f64("d4") = "d0"
& f64("d3") = "d0"
& f64("d2") = "d0"
& f64("d1") = "d0"
& f64("d0") = "d0"
& f63("d5") = "d0"
& f63("d4") = "d0"
& f63("d3") = "d0"
& f63("d2") = "d0"
& f63("d1") = "d0"
& f63("d0") = "d0"
& f62("d5") = "d0"
& f62("d4") = "d0"
& f62("d3") = "d0"
& f62("d2") = "d0"
& f62("d1") = "d0"
& f62("d0") = "d0"
& f61("d5") = "d0"
& f61("d4") = "d0"
& f61("d3") = "d0"
& f61("d2") = "d0"
& f61("d1") = "d0"
& f61("d0") = "d0"
& f60("d5") = "d0"
& f60("d4") = "d0"
& f60("d3") = "d0"
& f60("d2") = "d0"
& f60("d1") = "d0"
& f60("d0") = "d0"
& f59("d5") = "d0"
& f59("d4") = "d0"
& f59("d3") = "d0"
& f59("d2") = "d0"
& f59("d1") = "d0"
& f59("d0") = "d0"
& f58("d5") = "d0"
& f58("d4") = "d0"
& f58("d3") = "d0"
& f58("d2") = "d0"
& f58("d1") = "d0"
& f58("d0") = "d0"
& f57("d5") = "d0"
& f57("d4") = "d0"
& f57("d3") = "d0"
& f57("d2") = "d0"
& f57("d1") = "d0"
& f57("d0") = "d0"
& f56("d5") = "d0"
& f56("d4") = "d0"
& f56("d3") = "d0"
& f56("d2") = "d0"
& f56("d1") = "d0"
& f56("d0") = "d0"
& f55("d5") = "d0"
& f55("d4") = "d0"
& f55("d3") = "d0"
& f55("d2") = "d0"
& f55("d1") = "d0"
& f55("d0") = "d0"
& f54("d5") = "d0"
& f54("d4") = "d0"
& f54("d3") = "d0"
& f54("d2") = "d0"
& f54("d1") = "d0"
& f54("d0") = "d0"
& f53("d5") = "d0"
& f53("d4") = "d0"
& f53("d3") = "d0"
& f53("d2") = "d0"
& f53("d1") = "d0"
& f53("d0") = "d0"
& f52("d5") = "d0"
& f52("d4") = "d0"
& f52("d3") = "d0"
& f52("d2") = "d0"
& f52("d1") = "d0"
& f52("d0") = "d0"
& f51("d5") = "d0"
& f51("d4") = "d0"
& f51("d3") = "d0"
& f51("d2") = "d0"
& f51("d1") = "d0"
& f51("d0") = "d0"
& f50("d5") = "d0"
& f50("d4") = "d0"
& f50("d3") = "d0"
& f50("d2") = "d0"
& f50("d1") = "d0"
& f50("d0") = "d0"
& f49("d5") = "d0"
& f49("d4") = "d0"
& f49("d3") = "d0"
& f49("d2") = "d0"
& f49("d1") = "d0"
& f49("d0") = "d0"
& f48("d5") = "d0"
& f48("d4") = "d0"
& f48("d3") = "d0"
& f48("d2") = "d0"
& f48("d1") = "d0"
& f48("d0") = "d0"
& f47("d5") = "d0"
& f47("d4") = "d0"
& f47("d3") = "d0"
& f47("d2") = "d0"
& f47("d1") = "d0"
& f47("d0") = "d0"
& f46("d5") = "d0"
& f46("d4") = "d0"
& f46("d3") = "d0"
& f46("d2") = "d0"
& f46("d1") = "d0"
& f46("d0") = "d0"
& f45("d5") = "d0"
& f45("d4") = "d0"
& f45("d3") = "d0"
& f45("d2") = "d0"
& f45("d1") = "d0"
& f45("d0") = "d0"
& f44("d5") = "d0"
& f44("d4") = "d0"
& f44("d3") = "d0"
& f44("d2") = "d0"
& f44("d1") = "d0"
& f44("d0") = "d0"
& f43("d5") = "d0"
& f43("d4") = "d0"
& f43("d3") = "d0"
& f43("d2") = "d0"
& f43("d1") = "d0"
& f43("d0") = "d0"
& f42("d5") = "d0"
& f42("d4") = "d0"
& f42("d3") = "d0"
& f42("d2") = "d0"
& f42("d1") = "d0"
& f42("d0") = "d0"
& f41("d5") = "d0"
& f41("d4") = "d0"
& f41("d3") = "d0"
& f41("d2") = "d0"
& f41("d1") = "d0"
& f41("d0") = "d0"
& f40("d5") = "d0"
& f40("d4") = "d0"
& f40("d3") = "d0"
& f40("d2") = "d0"
& f40("d1") = "d0"
& f40("d0") = "d0"
& f39("d5") = "d0"
& f39("d4") = "d0"
& f39("d3") = "d0"
& f39("d2") = "d0"
& f39("d1") = "d0"
& f39("d0") = "d0"
& f38("d5") = "d0"
& f38("d4") = "d0"
& f38("d3") = "d0"
& f38("d2") = "d0"
& f38("d1") = "d0"
& f38("d0") = "d0"
& f37("d5") = "d0"
& f37("d4") = "d0"
& f37("d3") = "d0"
& f37("d2") = "d0"
& f37("d1") = "d0"
& f37("d0") = "d0"
& f36("d5") = "d0"
& f36("d4") = "d0"
& f36("d3") = "d0"
& f36("d2") = "d0"
& f36("d1") = "d0"
& f36("d0") = "d0"
& f35("d5") = "d0"
& f35("d4") = "d0"
& f35("d3") = "d0"
& f35("d2") = "d0"
& f35("d1") = "d0"
& f35("d0") = "d0"
& f34("d5") = "d0"
& f34("d4") = "d0"
& f34("d3") = "d0"
& f34("d2") = "d0"
& f34("d1") = "d0"
& f34("d0") = "d0"
& f33("d5") = "d0"
& f33("d4") = "d0"
& f33("d3") = "d0"
& f33("d2") = "d0"
& f33("d1") = "d0"
& f33("d0") = "d0"
& f32("d5") = "d0"
& f32("d4") = "d0"
& f32("d3") = "d0"
& f32("d2") = "d0"
& f32("d1") = "d0"
& f32("d0") = "d0"
& f31("d5") = "d0"
& f31("d4") = "d0"
& f31("d3") = "d0"
& f31("d2") = "d0"
& f31("d1") = "d0"
& f31("d0") = "d0"
& f30("d5") = "d0"
& f30("d4") = "d0"
& f30("d3") = "d0"
& f30("d2") = "d0"
& f30("d1") = "d0"
& f30("d0") = "d0"
& f29("d5") = "d0"
& f29("d4") = "d0"
& f29("d3") = "d0"
& f29("d2") = "d0"
& f29("d1") = "d0"
& f29("d0") = "d0"
& f28("d5") = "d0"
& f28("d4") = "d0"
& f28("d3") = "d0"
& f28("d2") = "d0"
& f28("d1") = "d0"
& f28("d0") = "d0"
& f27("d5") = "d0"
& f27("d4") = "d0"
& f27("d3") = "d0"
& f27("d2") = "d0"
& f27("d1") = "d0"
& f27("d0") = "d0"
& f26("d5") = "d0"
& f26("d4") = "d0"
& f26("d3") = "d0"
& f26("d2") = "d0"
& f26("d1") = "d0"
& f26("d0") = "d0"
& f25("d5") = "d0"
& f25("d4") = "d0"
& f25("d3") = "d0"
& f25("d2") = "d0"
& f25("d1") = "d0"
& f25("d0") = "d0"
& f24("d5") = "d0"
& f24("d4") = "d0"
& f24("d3") = "d0"
& f24("d2") = "d0"
& f24("d1") = "d0"
& f24("d0") = "d0"
& f23("d5") = "d0"
& f23("d4") = "d0"
& f23("d3") = "d0"
& f23("d2") = "d0"
& f23("d1") = "d0"
& f23("d0") = "d0"
& f22("d5") = "d0"
& f22("d4") = "d0"
& f22("d3") = "d0"
& f22("d2") = "d0"
& f22("d1") = "d0"
& f22("d0") = "d0"
& f21("d5") = "d0"
& f21("d4") = "d0"
& f21("d3") = "d0"
& f21("d2") = "d0"
& f21("d1") = "d0"
& f21("d0") = "d0"
& f20("d5") = "d0"
& f20("d4") = "d0"
& f20("d3") = "d0"
& f20("d2") = "d0"
& f20("d1") = "d0"
& f20("d0") = "d0"
& f19("d5") = "d0"
& f19("d4") = "d0"
& f19("d3") = "d0"
& f19("d2") = "d0"
& f19("d1") = "d0"
& f19("d0") = "d0"
& f18("d5") = "d0"
& f18("d4") = "d0"
& f18("d3") = "d0"
& f18("d2") = "d0"
& f18("d1") = "d0"
& f18("d0") = "d0"
& f17("d5") = "d0"
& f17("d4") = "d0"
& f17("d3") = "d0"
& f17("d2") = "d0"
& f17("d1") = "d0"
& f17("d0") = "d0"
& f16("d5") = "d0"
& f16("d4") = "d0"
& f16("d3") = "d0"
& f16("d2") = "d0"
& f16("d1") = "d0"
& f16("d0") = "d0"
& f15("d5") = "d0"
& f15("d4") = "d0"
& f15("d3") = "d0"
& f15("d2") = "d0"
& f15("d1") = "d0"
& f15("d0") = "d0"
& f14("d5") = "d0"
& f14("d4") = "d0"
& f14("d3") = "d0"
& f14("d2") = "d0"
& f14("d1") = "d0"
& f14("d0") = "d0"
& f13("d5") = "d0"
& f13("d4") = "d0"
& f13("d3") = "d0"
& f13("d2") = "d0"
& f13("d1") = "d0"
& f13("d0") = "d0"
& f12("d5") = "d0"
& f12("d4") = "d0"
& f12("d3") = "d0"
& f12("d2") = "d0"
& f12("d1") = "d0"
& f12("d0") = "d0"
& f11("d5") = "d0"
& f11("d4") = "d0"
& f11("d3") = "d0"
& f11("d2") = "d0"
& f11("d1") = "d0"
& f11("d0") = "d0"
& f10("d5") = "d0"
& f10("d4") = "d0"
& f10("d3") = "d0"
& f10("d2") = "d0"
& f10("d1") = "d0"
& f10("d0") = "d0"
& f9("d5") = "d0"
& f9("d4") = "d0"
& f9("d3") = "d0"
& f9("d2") = "d0"
& f9("d1") = "d0"
& f9("d0") = "d0"
& f8("d5") = "d0"
& f8("d4") = "d0"
& f8("d3") = "d0"
& f8("d2") = "d0"
& f8("d1") = "d0"
& f8("d0") = "d0"
& f7("d5") = "d0"
& f7("d4") = "d0"
& f7("d3") = "d0"
& f7("d2") = "d0"
& f7("d1") = "d0"
& f7("d0") = "d0"
& f6("d5") = "d0"
& f6("d4") = "d0"
& f6("d3") = "d0"
& f6("d2") = "d0"
& f6("d1") = "d0"
& f6("d0") = "d0"
& f5("d5") = "d0"
& f5("d4") = "d0"
& f5("d3") = "d0"
& f5("d2") = "d0"
& f5("d1") = "d0"
& f5("d0") = "d0"
& f4("d5") = "d0"
& f4("d4") = "d0"
& f4("d3") = "d0"
& f4("d2") = "d0"
& f4("d1") = "d0"
& f4("d0") = "d0"
& f3("d5") = "d0"
& f3("d4") = "d0"
& f3("d3") = "d0"
& f3("d2") = "d0"
& f3("d1") = "d0"
& f3("d0") = "d0"
& f2("d5") = "d0"
& f2("d4") = "d0"
& f2("d3") = "d0"
& f2("d2") = "d0"
& f2("d1") = "d0"
& f2("d0") = "d0"
& f1("d5") = "d0"
& f1("d4") = "d0"
& f1("d3") = "d0"
& f1("d2") = "d0"
& f1("d1") = "d0"
& f1("d0") = "d0"
& c2 = "d1"
& c1 = "d0" ) ).
fof(interp_relations,interpretation-mappings,
( ~ iisToppingOf("d5","d5")
& ~ iisToppingOf("d5","d4")
& ~ iisToppingOf("d5","d3")
& ~ iisToppingOf("d5","d2")
& ~ iisToppingOf("d5","d1")
& ~ iisToppingOf("d5","d0")
& ~ iisToppingOf("d4","d5")
& ~ iisToppingOf("d4","d4")
& ~ iisToppingOf("d4","d3")
& ~ iisToppingOf("d4","d2")
& ~ iisToppingOf("d4","d1")
& ~ iisToppingOf("d4","d0")
& ~ iisToppingOf("d3","d5")
& ~ iisToppingOf("d3","d4")
& ~ iisToppingOf("d3","d3")
& ~ iisToppingOf("d3","d2")
& ~ iisToppingOf("d3","d1")
& ~ iisToppingOf("d3","d0")
& ~ iisToppingOf("d2","d5")
& ~ iisToppingOf("d2","d4")
& ~ iisToppingOf("d2","d3")
& ~ iisToppingOf("d2","d2")
& ~ iisToppingOf("d2","d1")
& ~ iisToppingOf("d2","d0")
& ~ iisToppingOf("d1","d5")
& ~ iisToppingOf("d1","d4")
& ~ iisToppingOf("d1","d3")
& ~ iisToppingOf("d1","d2")
& ~ iisToppingOf("d1","d1")
& ~ iisToppingOf("d1","d0")
& ~ iisToppingOf("d0","d5")
& ~ iisToppingOf("d0","d4")
& ~ iisToppingOf("d0","d3")
& ~ iisToppingOf("d0","d2")
& ~ iisToppingOf("d0","d1")
& ~ iisToppingOf("d0","d0")
& ~ iisIngredientOf("d5","d5")
& ~ iisIngredientOf("d5","d4")
& ~ iisIngredientOf("d5","d3")
& ~ iisIngredientOf("d5","d2")
& ~ iisIngredientOf("d5","d1")
& ~ iisIngredientOf("d5","d0")
& ~ iisIngredientOf("d4","d5")
& ~ iisIngredientOf("d4","d4")
& ~ iisIngredientOf("d4","d3")
& ~ iisIngredientOf("d4","d2")
& ~ iisIngredientOf("d4","d1")
& ~ iisIngredientOf("d4","d0")
& ~ iisIngredientOf("d3","d5")
& ~ iisIngredientOf("d3","d4")
& ~ iisIngredientOf("d3","d3")
& ~ iisIngredientOf("d3","d2")
& ~ iisIngredientOf("d3","d1")
& ~ iisIngredientOf("d3","d0")
& ~ iisIngredientOf("d2","d5")
& ~ iisIngredientOf("d2","d4")
& ~ iisIngredientOf("d2","d3")
& ~ iisIngredientOf("d2","d2")
& ~ iisIngredientOf("d2","d1")
& ~ iisIngredientOf("d2","d0")
& ~ iisIngredientOf("d1","d5")
& ~ iisIngredientOf("d1","d4")
& ~ iisIngredientOf("d1","d3")
& ~ iisIngredientOf("d1","d2")
& ~ iisIngredientOf("d1","d1")
& ~ iisIngredientOf("d1","d0")
& ~ iisIngredientOf("d0","d5")
& ~ iisIngredientOf("d0","d4")
& ~ iisIngredientOf("d0","d3")
& ~ iisIngredientOf("d0","d2")
& ~ iisIngredientOf("d0","d1")
& ~ iisIngredientOf("d0","d0")
& ~ iisBaseOf("d5","d5")
& ~ iisBaseOf("d5","d4")
& ~ iisBaseOf("d5","d3")
& ~ iisBaseOf("d5","d2")
& ~ iisBaseOf("d5","d1")
& ~ iisBaseOf("d5","d0")
& ~ iisBaseOf("d4","d5")
& ~ iisBaseOf("d4","d4")
& ~ iisBaseOf("d4","d3")
& ~ iisBaseOf("d4","d2")
& ~ iisBaseOf("d4","d1")
& ~ iisBaseOf("d4","d0")
& ~ iisBaseOf("d3","d5")
& ~ iisBaseOf("d3","d4")
& ~ iisBaseOf("d3","d3")
& ~ iisBaseOf("d3","d2")
& ~ iisBaseOf("d3","d1")
& ~ iisBaseOf("d3","d0")
& ~ iisBaseOf("d2","d5")
& ~ iisBaseOf("d2","d4")
& ~ iisBaseOf("d2","d3")
& ~ iisBaseOf("d2","d2")
& ~ iisBaseOf("d2","d1")
& ~ iisBaseOf("d2","d0")
& ~ iisBaseOf("d1","d5")
& ~ iisBaseOf("d1","d4")
& ~ iisBaseOf("d1","d3")
& ~ iisBaseOf("d1","d2")
& ~ iisBaseOf("d1","d1")
& ~ iisBaseOf("d1","d0")
& ~ iisBaseOf("d0","d5")
& ~ iisBaseOf("d0","d4")
& ~ iisBaseOf("d0","d3")
& ~ iisBaseOf("d0","d2")
& ~ iisBaseOf("d0","d1")
& ~ iisBaseOf("d0","d0")
& ~ ihasTopping("d5","d5")
& ~ ihasTopping("d5","d4")
& ~ ihasTopping("d5","d3")
& ~ ihasTopping("d5","d2")
& ~ ihasTopping("d5","d1")
& ~ ihasTopping("d5","d0")
& ~ ihasTopping("d4","d5")
& ~ ihasTopping("d4","d4")
& ~ ihasTopping("d4","d3")
& ~ ihasTopping("d4","d2")
& ~ ihasTopping("d4","d1")
& ~ ihasTopping("d4","d0")
& ~ ihasTopping("d3","d5")
& ~ ihasTopping("d3","d4")
& ~ ihasTopping("d3","d3")
& ~ ihasTopping("d3","d2")
& ~ ihasTopping("d3","d1")
& ~ ihasTopping("d3","d0")
& ~ ihasTopping("d2","d5")
& ~ ihasTopping("d2","d4")
& ~ ihasTopping("d2","d3")
& ~ ihasTopping("d2","d2")
& ~ ihasTopping("d2","d1")
& ~ ihasTopping("d2","d0")
& ~ ihasTopping("d1","d5")
& ~ ihasTopping("d1","d4")
& ~ ihasTopping("d1","d3")
& ~ ihasTopping("d1","d2")
& ~ ihasTopping("d1","d1")
& ~ ihasTopping("d1","d0")
& ~ ihasTopping("d0","d5")
& ~ ihasTopping("d0","d4")
& ~ ihasTopping("d0","d3")
& ~ ihasTopping("d0","d2")
& ~ ihasTopping("d0","d1")
& ~ ihasTopping("d0","d0")
& ~ ihasSpiciness("d5","d5")
& ~ ihasSpiciness("d5","d4")
& ~ ihasSpiciness("d5","d3")
& ~ ihasSpiciness("d5","d2")
& ~ ihasSpiciness("d5","d1")
& ~ ihasSpiciness("d5","d0")
& ~ ihasSpiciness("d4","d5")
& ~ ihasSpiciness("d4","d4")
& ~ ihasSpiciness("d4","d3")
& ~ ihasSpiciness("d4","d2")
& ~ ihasSpiciness("d4","d1")
& ~ ihasSpiciness("d4","d0")
& ~ ihasSpiciness("d3","d5")
& ~ ihasSpiciness("d3","d4")
& ~ ihasSpiciness("d3","d3")
& ~ ihasSpiciness("d3","d2")
& ~ ihasSpiciness("d3","d1")
& ~ ihasSpiciness("d3","d0")
& ~ ihasSpiciness("d2","d5")
& ~ ihasSpiciness("d2","d4")
& ~ ihasSpiciness("d2","d3")
& ~ ihasSpiciness("d2","d2")
& ~ ihasSpiciness("d2","d1")
& ~ ihasSpiciness("d2","d0")
& ~ ihasSpiciness("d1","d5")
& ~ ihasSpiciness("d1","d4")
& ~ ihasSpiciness("d1","d3")
& ~ ihasSpiciness("d1","d2")
& ~ ihasSpiciness("d1","d1")
& ~ ihasSpiciness("d1","d0")
& ~ ihasSpiciness("d0","d5")
& ~ ihasSpiciness("d0","d4")
& ~ ihasSpiciness("d0","d3")
& ~ ihasSpiciness("d0","d2")
& ~ ihasSpiciness("d0","d1")
& ~ ihasSpiciness("d0","d0")
& ~ ihasIngredient("d5","d5")
& ~ ihasIngredient("d5","d4")
& ~ ihasIngredient("d5","d3")
& ~ ihasIngredient("d5","d2")
& ~ ihasIngredient("d5","d1")
& ~ ihasIngredient("d5","d0")
& ~ ihasIngredient("d4","d5")
& ~ ihasIngredient("d4","d4")
& ~ ihasIngredient("d4","d3")
& ~ ihasIngredient("d4","d2")
& ~ ihasIngredient("d4","d1")
& ~ ihasIngredient("d4","d0")
& ~ ihasIngredient("d3","d5")
& ~ ihasIngredient("d3","d4")
& ~ ihasIngredient("d3","d3")
& ~ ihasIngredient("d3","d2")
& ~ ihasIngredient("d3","d1")
& ~ ihasIngredient("d3","d0")
& ~ ihasIngredient("d2","d5")
& ~ ihasIngredient("d2","d4")
& ~ ihasIngredient("d2","d3")
& ~ ihasIngredient("d2","d2")
& ~ ihasIngredient("d2","d1")
& ~ ihasIngredient("d2","d0")
& ~ ihasIngredient("d1","d5")
& ~ ihasIngredient("d1","d4")
& ~ ihasIngredient("d1","d3")
& ~ ihasIngredient("d1","d2")
& ~ ihasIngredient("d1","d1")
& ~ ihasIngredient("d1","d0")
& ~ ihasIngredient("d0","d5")
& ~ ihasIngredient("d0","d4")
& ~ ihasIngredient("d0","d3")
& ~ ihasIngredient("d0","d2")
& ~ ihasIngredient("d0","d1")
& ~ ihasIngredient("d0","d0")
& ~ ihasCountryOfOrigin("d5","d5")
& ~ ihasCountryOfOrigin("d5","d4")
& ~ ihasCountryOfOrigin("d5","d3")
& ~ ihasCountryOfOrigin("d5","d2")
& ~ ihasCountryOfOrigin("d5","d1")
& ~ ihasCountryOfOrigin("d5","d0")
& ~ ihasCountryOfOrigin("d4","d5")
& ~ ihasCountryOfOrigin("d4","d4")
& ~ ihasCountryOfOrigin("d4","d3")
& ~ ihasCountryOfOrigin("d4","d2")
& ~ ihasCountryOfOrigin("d4","d1")
& ~ ihasCountryOfOrigin("d4","d0")
& ~ ihasCountryOfOrigin("d3","d5")
& ~ ihasCountryOfOrigin("d3","d4")
& ~ ihasCountryOfOrigin("d3","d3")
& ~ ihasCountryOfOrigin("d3","d2")
& ~ ihasCountryOfOrigin("d3","d1")
& ~ ihasCountryOfOrigin("d3","d0")
& ~ ihasCountryOfOrigin("d2","d5")
& ~ ihasCountryOfOrigin("d2","d4")
& ~ ihasCountryOfOrigin("d2","d3")
& ~ ihasCountryOfOrigin("d2","d2")
& ~ ihasCountryOfOrigin("d2","d1")
& ~ ihasCountryOfOrigin("d2","d0")
& ~ ihasCountryOfOrigin("d1","d5")
& ~ ihasCountryOfOrigin("d1","d4")
& ~ ihasCountryOfOrigin("d1","d3")
& ~ ihasCountryOfOrigin("d1","d2")
& ~ ihasCountryOfOrigin("d1","d1")
& ~ ihasCountryOfOrigin("d1","d0")
& ~ ihasCountryOfOrigin("d0","d5")
& ~ ihasCountryOfOrigin("d0","d4")
& ~ ihasCountryOfOrigin("d0","d3")
& ~ ihasCountryOfOrigin("d0","d2")
& ~ ihasCountryOfOrigin("d0","d1")
& ~ ihasCountryOfOrigin("d0","d0")
& ~ ihasBase("d5","d5")
& ~ ihasBase("d5","d4")
& ~ ihasBase("d5","d3")
& ~ ihasBase("d5","d2")
& ~ ihasBase("d5","d1")
& ~ ihasBase("d5","d0")
& ~ ihasBase("d4","d5")
& ~ ihasBase("d4","d4")
& ~ ihasBase("d4","d3")
& ~ ihasBase("d4","d2")
& ~ ihasBase("d4","d1")
& ~ ihasBase("d4","d0")
& ~ ihasBase("d3","d5")
& ~ ihasBase("d3","d4")
& ~ ihasBase("d3","d3")
& ~ ihasBase("d3","d2")
& ~ ihasBase("d3","d1")
& ~ ihasBase("d3","d0")
& ~ ihasBase("d2","d5")
& ~ ihasBase("d2","d4")
& ~ ihasBase("d2","d3")
& ~ ihasBase("d2","d2")
& ~ ihasBase("d2","d1")
& ~ ihasBase("d2","d0")
& ~ ihasBase("d1","d5")
& ~ ihasBase("d1","d4")
& ~ ihasBase("d1","d3")
& ~ ihasBase("d1","d2")
& ~ ihasBase("d1","d1")
& ~ ihasBase("d1","d0")
& ~ ihasBase("d0","d5")
& ~ ihasBase("d0","d4")
& ~ ihasBase("d0","d3")
& ~ ihasBase("d0","d2")
& ~ ihasBase("d0","d1")
& ~ ihasBase("d0","d0")
& ~ xsd_string("d5")
& ~ xsd_string("d4")
& ~ xsd_string("d3")
& ~ xsd_string("d2")
& ~ xsd_string("d1")
& ~ xsd_string("d0")
& ~ xsd_integer("d5")
& ~ xsd_integer("d4")
& ~ xsd_integer("d3")
& ~ xsd_integer("d2")
& ~ xsd_integer("d1")
& ~ xsd_integer("d0")
& iowlThing("d5")
& iowlThing("d4")
& iowlThing("d3")
& iowlThing("d2")
& ~ iowlThing("d1")
& iowlThing("d0")
& ~ iowlNothing("d5")
& ~ iowlNothing("d4")
& ~ iowlNothing("d3")
& ~ iowlNothing("d2")
& ~ iowlNothing("d1")
& ~ iowlNothing("d0")
& ~ iVeneziana("d5")
& ~ iVeneziana("d4")
& ~ iVeneziana("d3")
& ~ iVeneziana("d2")
& ~ iVeneziana("d1")
& ~ iVeneziana("d0")
& ~ iVegetarianTopping("d5")
& ~ iVegetarianTopping("d4")
& ~ iVegetarianTopping("d3")
& ~ iVegetarianTopping("d2")
& ~ iVegetarianTopping("d1")
& ~ iVegetarianTopping("d0")
& ~ iVegetarianPizzaEquivalent2("d5")
& ~ iVegetarianPizzaEquivalent2("d4")
& ~ iVegetarianPizzaEquivalent2("d3")
& ~ iVegetarianPizzaEquivalent2("d2")
& ~ iVegetarianPizzaEquivalent2("d1")
& ~ iVegetarianPizzaEquivalent2("d0")
& ~ iVegetarianPizzaEquivalent1("d5")
& ~ iVegetarianPizzaEquivalent1("d4")
& ~ iVegetarianPizzaEquivalent1("d3")
& ~ iVegetarianPizzaEquivalent1("d2")
& ~ iVegetarianPizzaEquivalent1("d1")
& ~ iVegetarianPizzaEquivalent1("d0")
& ~ iVegetarianPizza("d5")
& ~ iVegetarianPizza("d4")
& ~ iVegetarianPizza("d3")
& ~ iVegetarianPizza("d2")
& ~ iVegetarianPizza("d1")
& ~ iVegetarianPizza("d0")
& ~ iVegetableTopping("d5")
& ~ iVegetableTopping("d4")
& ~ iVegetableTopping("d3")
& ~ iVegetableTopping("d2")
& ~ iVegetableTopping("d1")
& ~ iVegetableTopping("d0")
& ~ iValuePartition("d5")
& ~ iValuePartition("d4")
& ~ iValuePartition("d3")
& ~ iValuePartition("d2")
& ~ iValuePartition("d1")
& ~ iValuePartition("d0")
& ~ iUnclosedPizza("d5")
& ~ iUnclosedPizza("d4")
& ~ iUnclosedPizza("d3")
& ~ iUnclosedPizza("d2")
& ~ iUnclosedPizza("d1")
& ~ iUnclosedPizza("d0")
& ~ iTomatoTopping("d5")
& ~ iTomatoTopping("d4")
& ~ iTomatoTopping("d3")
& ~ iTomatoTopping("d2")
& ~ iTomatoTopping("d1")
& ~ iTomatoTopping("d0")
& ~ iTobascoPepperSauce("d5")
& ~ iTobascoPepperSauce("d4")
& ~ iTobascoPepperSauce("d3")
& ~ iTobascoPepperSauce("d2")
& ~ iTobascoPepperSauce("d1")
& ~ iTobascoPepperSauce("d0")
& ~ iThinAndCrispyPizza("d5")
& ~ iThinAndCrispyPizza("d4")
& ~ iThinAndCrispyPizza("d3")
& ~ iThinAndCrispyPizza("d2")
& ~ iThinAndCrispyPizza("d1")
& ~ iThinAndCrispyPizza("d0")
& ~ iThinAndCrispyBase("d5")
& ~ iThinAndCrispyBase("d4")
& ~ iThinAndCrispyBase("d3")
& ~ iThinAndCrispyBase("d2")
& ~ iThinAndCrispyBase("d1")
& ~ iThinAndCrispyBase("d0")
& ~ iSweetPepperTopping("d5")
& ~ iSweetPepperTopping("d4")
& ~ iSweetPepperTopping("d3")
& ~ iSweetPepperTopping("d2")
& ~ iSweetPepperTopping("d1")
& ~ iSweetPepperTopping("d0")
& ~ iSundriedTomatoTopping("d5")
& ~ iSundriedTomatoTopping("d4")
& ~ iSundriedTomatoTopping("d3")
& ~ iSundriedTomatoTopping("d2")
& ~ iSundriedTomatoTopping("d1")
& ~ iSundriedTomatoTopping("d0")
& ~ iSultanaTopping("d5")
& ~ iSultanaTopping("d4")
& ~ iSultanaTopping("d3")
& ~ iSultanaTopping("d2")
& ~ iSultanaTopping("d1")
& ~ iSultanaTopping("d0")
& ~ iSpinachTopping("d5")
& ~ iSpinachTopping("d4")
& ~ iSpinachTopping("d3")
& ~ iSpinachTopping("d2")
& ~ iSpinachTopping("d1")
& ~ iSpinachTopping("d0")
& ~ iSpicyTopping("d5")
& ~ iSpicyTopping("d4")
& ~ iSpicyTopping("d3")
& ~ iSpicyTopping("d2")
& ~ iSpicyTopping("d1")
& ~ iSpicyTopping("d0")
& ~ iSpicyPizzaEquivalent("d5")
& ~ iSpicyPizzaEquivalent("d4")
& ~ iSpicyPizzaEquivalent("d3")
& ~ iSpicyPizzaEquivalent("d2")
& ~ iSpicyPizzaEquivalent("d1")
& ~ iSpicyPizzaEquivalent("d0")
& ~ iSpicyPizza("d5")
& ~ iSpicyPizza("d4")
& ~ iSpicyPizza("d3")
& ~ iSpicyPizza("d2")
& ~ iSpicyPizza("d1")
& ~ iSpicyPizza("d0")
& ~ iSpiciness("d5")
& ~ iSpiciness("d4")
& ~ iSpiciness("d3")
& ~ iSpiciness("d2")
& ~ iSpiciness("d1")
& ~ iSpiciness("d0")
& ~ iSoho("d5")
& ~ iSoho("d4")
& ~ iSoho("d3")
& ~ iSoho("d2")
& ~ iSoho("d1")
& ~ iSoho("d0")
& ~ iSloppyGiuseppe("d5")
& ~ iSloppyGiuseppe("d4")
& ~ iSloppyGiuseppe("d3")
& ~ iSloppyGiuseppe("d2")
& ~ iSloppyGiuseppe("d1")
& ~ iSloppyGiuseppe("d0")
& ~ iSlicedTomatoTopping("d5")
& ~ iSlicedTomatoTopping("d4")
& ~ iSlicedTomatoTopping("d3")
& ~ iSlicedTomatoTopping("d2")
& ~ iSlicedTomatoTopping("d1")
& ~ iSlicedTomatoTopping("d0")
& ~ iSiciliana("d5")
& ~ iSiciliana("d4")
& ~ iSiciliana("d3")
& ~ iSiciliana("d2")
& ~ iSiciliana("d1")
& ~ iSiciliana("d0")
& ~ iSauceTopping("d5")
& ~ iSauceTopping("d4")
& ~ iSauceTopping("d3")
& ~ iSauceTopping("d2")
& ~ iSauceTopping("d1")
& ~ iSauceTopping("d0")
& ~ iRosemaryTopping("d5")
& ~ iRosemaryTopping("d4")
& ~ iRosemaryTopping("d3")
& ~ iRosemaryTopping("d2")
& ~ iRosemaryTopping("d1")
& ~ iRosemaryTopping("d0")
& ~ iRosa("d5")
& ~ iRosa("d4")
& ~ iRosa("d3")
& ~ iRosa("d2")
& ~ iRosa("d1")
& ~ iRosa("d0")
& ~ iRocketTopping("d5")
& ~ iRocketTopping("d4")
& ~ iRocketTopping("d3")
& ~ iRocketTopping("d2")
& ~ iRocketTopping("d1")
& ~ iRocketTopping("d0")
& ~ iRedOnionTopping("d5")
& ~ iRedOnionTopping("d4")
& ~ iRedOnionTopping("d3")
& ~ iRedOnionTopping("d2")
& ~ iRedOnionTopping("d1")
& ~ iRedOnionTopping("d0")
& ~ iRealItalianPizza("d5")
& ~ iRealItalianPizza("d4")
& ~ iRealItalianPizza("d3")
& ~ iRealItalianPizza("d2")
& ~ iRealItalianPizza("d1")
& ~ iRealItalianPizza("d0")
& ~ iQuattroFormaggi("d5")
& ~ iQuattroFormaggi("d4")
& ~ iQuattroFormaggi("d3")
& ~ iQuattroFormaggi("d2")
& ~ iQuattroFormaggi("d1")
& ~ iQuattroFormaggi("d0")
& ~ iPrinceCarlo("d5")
& ~ iPrinceCarlo("d4")
& ~ iPrinceCarlo("d3")
& ~ iPrinceCarlo("d2")
& ~ iPrinceCarlo("d1")
& ~ iPrinceCarlo("d0")
& ~ iPrawnsTopping("d5")
& ~ iPrawnsTopping("d4")
& ~ iPrawnsTopping("d3")
& ~ iPrawnsTopping("d2")
& ~ iPrawnsTopping("d1")
& ~ iPrawnsTopping("d0")
& ~ iPolloAdAstra("d5")
& ~ iPolloAdAstra("d4")
& ~ iPolloAdAstra("d3")
& ~ iPolloAdAstra("d2")
& ~ iPolloAdAstra("d1")
& ~ iPolloAdAstra("d0")
& ~ iPizzaTopping("d5")
& ~ iPizzaTopping("d4")
& ~ iPizzaTopping("d3")
& ~ iPizzaTopping("d2")
& ~ iPizzaTopping("d1")
& ~ iPizzaTopping("d0")
& ~ iPizzaBase("d5")
& ~ iPizzaBase("d4")
& ~ iPizzaBase("d3")
& ~ iPizzaBase("d2")
& ~ iPizzaBase("d1")
& ~ iPizzaBase("d0")
& ~ iPizza("d5")
& ~ iPizza("d4")
& ~ iPizza("d3")
& ~ iPizza("d2")
& ~ iPizza("d1")
& ~ iPizza("d0")
& ~ iPineKernels("d5")
& ~ iPineKernels("d4")
& ~ iPineKernels("d3")
& ~ iPineKernels("d2")
& ~ iPineKernels("d1")
& ~ iPineKernels("d0")
& ~ iPetitPoisTopping("d5")
& ~ iPetitPoisTopping("d4")
& ~ iPetitPoisTopping("d3")
& ~ iPetitPoisTopping("d2")
& ~ iPetitPoisTopping("d1")
& ~ iPetitPoisTopping("d0")
& ~ iPepperTopping("d5")
& ~ iPepperTopping("d4")
& ~ iPepperTopping("d3")
& ~ iPepperTopping("d2")
& ~ iPepperTopping("d1")
& ~ iPepperTopping("d0")
& ~ iPeperoniSausageTopping("d5")
& ~ iPeperoniSausageTopping("d4")
& ~ iPeperoniSausageTopping("d3")
& ~ iPeperoniSausageTopping("d2")
& ~ iPeperoniSausageTopping("d1")
& ~ iPeperoniSausageTopping("d0")
& ~ iPeperonataTopping("d5")
& ~ iPeperonataTopping("d4")
& ~ iPeperonataTopping("d3")
& ~ iPeperonataTopping("d2")
& ~ iPeperonataTopping("d1")
& ~ iPeperonataTopping("d0")
& ~ iParmesanTopping("d5")
& ~ iParmesanTopping("d4")
& ~ iParmesanTopping("d3")
& ~ iParmesanTopping("d2")
& ~ iParmesanTopping("d1")
& ~ iParmesanTopping("d0")
& ~ iParmense("d5")
& ~ iParmense("d4")
& ~ iParmense("d3")
& ~ iParmense("d2")
& ~ iParmense("d1")
& ~ iParmense("d0")
& ~ iParmaHamTopping("d5")
& ~ iParmaHamTopping("d4")
& ~ iParmaHamTopping("d3")
& ~ iParmaHamTopping("d2")
& ~ iParmaHamTopping("d1")
& ~ iParmaHamTopping("d0")
& ~ iOnionTopping("d5")
& ~ iOnionTopping("d4")
& ~ iOnionTopping("d3")
& ~ iOnionTopping("d2")
& ~ iOnionTopping("d1")
& ~ iOnionTopping("d0")
& ~ iOliveTopping("d5")
& ~ iOliveTopping("d4")
& ~ iOliveTopping("d3")
& ~ iOliveTopping("d2")
& ~ iOliveTopping("d1")
& ~ iOliveTopping("d0")
& ~ iNutTopping("d5")
& ~ iNutTopping("d4")
& ~ iNutTopping("d3")
& ~ iNutTopping("d2")
& ~ iNutTopping("d1")
& ~ iNutTopping("d0")
& ~ iNonVegetarianPizza("d5")
& ~ iNonVegetarianPizza("d4")
& ~ iNonVegetarianPizza("d3")
& ~ iNonVegetarianPizza("d2")
& ~ iNonVegetarianPizza("d1")
& ~ iNonVegetarianPizza("d0")
& ~ iNapoletana("d5")
& ~ iNapoletana("d4")
& ~ iNapoletana("d3")
& ~ iNapoletana("d2")
& ~ iNapoletana("d1")
& ~ iNapoletana("d0")
& ~ iNamedPizza("d5")
& ~ iNamedPizza("d4")
& ~ iNamedPizza("d3")
& ~ iNamedPizza("d2")
& ~ iNamedPizza("d1")
& ~ iNamedPizza("d0")
& ~ iMushroomTopping("d5")
& ~ iMushroomTopping("d4")
& ~ iMushroomTopping("d3")
& ~ iMushroomTopping("d2")
& ~ iMushroomTopping("d1")
& ~ iMushroomTopping("d0")
& ~ iMushroom("d5")
& ~ iMushroom("d4")
& ~ iMushroom("d3")
& ~ iMushroom("d2")
& ~ iMushroom("d1")
& ~ iMushroom("d0")
& ~ iMozzarellaTopping("d5")
& ~ iMozzarellaTopping("d4")
& ~ iMozzarellaTopping("d3")
& ~ iMozzarellaTopping("d2")
& ~ iMozzarellaTopping("d1")
& ~ iMozzarellaTopping("d0")
& ~ iMixedSeafoodTopping("d5")
& ~ iMixedSeafoodTopping("d4")
& ~ iMixedSeafoodTopping("d3")
& ~ iMixedSeafoodTopping("d2")
& ~ iMixedSeafoodTopping("d1")
& ~ iMixedSeafoodTopping("d0")
& ~ iMild("d5")
& ~ iMild("d4")
& ~ iMild("d3")
& ~ iMild("d2")
& ~ iMild("d1")
& ~ iMild("d0")
& ~ iMedium("d5")
& ~ iMedium("d4")
& ~ iMedium("d3")
& ~ iMedium("d2")
& ~ iMedium("d1")
& ~ iMedium("d0")
& ~ iMeatyPizza("d5")
& ~ iMeatyPizza("d4")
& ~ iMeatyPizza("d3")
& ~ iMeatyPizza("d2")
& ~ iMeatyPizza("d1")
& ~ iMeatyPizza("d0")
& ~ iMeatTopping("d5")
& ~ iMeatTopping("d4")
& ~ iMeatTopping("d3")
& ~ iMeatTopping("d2")
& ~ iMeatTopping("d1")
& ~ iMeatTopping("d0")
& ~ iMargherita("d5")
& ~ iMargherita("d4")
& ~ iMargherita("d3")
& ~ iMargherita("d2")
& ~ iMargherita("d1")
& ~ iMargherita("d0")
& ~ iLeekTopping("d5")
& ~ iLeekTopping("d4")
& ~ iLeekTopping("d3")
& ~ iLeekTopping("d2")
& ~ iLeekTopping("d1")
& ~ iLeekTopping("d0")
& ~ iLaReine("d5")
& ~ iLaReine("d4")
& ~ iLaReine("d3")
& ~ iLaReine("d2")
& ~ iLaReine("d1")
& ~ iLaReine("d0")
& ~ iJalapenoPepperTopping("d5")
& ~ iJalapenoPepperTopping("d4")
& ~ iJalapenoPepperTopping("d3")
& ~ iJalapenoPepperTopping("d2")
& ~ iJalapenoPepperTopping("d1")
& ~ iJalapenoPepperTopping("d0")
& ~ iInterestingPizza("d5")
& ~ iInterestingPizza("d4")
& ~ iInterestingPizza("d3")
& ~ iInterestingPizza("d2")
& ~ iInterestingPizza("d1")
& ~ iInterestingPizza("d0")
& ~ iIceCream("d5")
& ~ iIceCream("d4")
& ~ iIceCream("d3")
& ~ iIceCream("d2")
& ~ iIceCream("d1")
& ~ iIceCream("d0")
& ~ iHotSpicedBeefTopping("d5")
& ~ iHotSpicedBeefTopping("d4")
& ~ iHotSpicedBeefTopping("d3")
& ~ iHotSpicedBeefTopping("d2")
& ~ iHotSpicedBeefTopping("d1")
& ~ iHotSpicedBeefTopping("d0")
& ~ iHotGreenPepperTopping("d5")
& ~ iHotGreenPepperTopping("d4")
& ~ iHotGreenPepperTopping("d3")
& ~ iHotGreenPepperTopping("d2")
& ~ iHotGreenPepperTopping("d1")
& ~ iHotGreenPepperTopping("d0")
& ~ iHot("d5")
& ~ iHot("d4")
& ~ iHot("d3")
& ~ iHot("d2")
& ~ iHot("d1")
& ~ iHot("d0")
& ~ iHerbSpiceTopping("d5")
& ~ iHerbSpiceTopping("d4")
& ~ iHerbSpiceTopping("d3")
& ~ iHerbSpiceTopping("d2")
& ~ iHerbSpiceTopping("d1")
& ~ iHerbSpiceTopping("d0")
& ~ iHamTopping("d5")
& ~ iHamTopping("d4")
& ~ iHamTopping("d3")
& ~ iHamTopping("d2")
& ~ iHamTopping("d1")
& ~ iHamTopping("d0")
& ~ iGreenPepperTopping("d5")
& ~ iGreenPepperTopping("d4")
& ~ iGreenPepperTopping("d3")
& ~ iGreenPepperTopping("d2")
& ~ iGreenPepperTopping("d1")
& ~ iGreenPepperTopping("d0")
& ~ iGorgonzolaTopping("d5")
& ~ iGorgonzolaTopping("d4")
& ~ iGorgonzolaTopping("d3")
& ~ iGorgonzolaTopping("d2")
& ~ iGorgonzolaTopping("d1")
& ~ iGorgonzolaTopping("d0")
& ~ iGoatsCheeseTopping("d5")
& ~ iGoatsCheeseTopping("d4")
& ~ iGoatsCheeseTopping("d3")
& ~ iGoatsCheeseTopping("d2")
& ~ iGoatsCheeseTopping("d1")
& ~ iGoatsCheeseTopping("d0")
& ~ iGiardiniera("d5")
& ~ iGiardiniera("d4")
& ~ iGiardiniera("d3")
& ~ iGiardiniera("d2")
& ~ iGiardiniera("d1")
& ~ iGiardiniera("d0")
& ~ iGarlicTopping("d5")
& ~ iGarlicTopping("d4")
& ~ iGarlicTopping("d3")
& ~ iGarlicTopping("d2")
& ~ iGarlicTopping("d1")
& ~ iGarlicTopping("d0")
& ~ iFruttiDiMare("d5")
& ~ iFruttiDiMare("d4")
& ~ iFruttiDiMare("d3")
& ~ iFruttiDiMare("d2")
& ~ iFruttiDiMare("d1")
& ~ iFruttiDiMare("d0")
& ~ iFruitTopping("d5")
& ~ iFruitTopping("d4")
& ~ iFruitTopping("d3")
& ~ iFruitTopping("d2")
& ~ iFruitTopping("d1")
& ~ iFruitTopping("d0")
& ~ iFourSeasons("d5")
& ~ iFourSeasons("d4")
& ~ iFourSeasons("d3")
& ~ iFourSeasons("d2")
& ~ iFourSeasons("d1")
& ~ iFourSeasons("d0")
& ~ iFourCheesesTopping("d5")
& ~ iFourCheesesTopping("d4")
& ~ iFourCheesesTopping("d3")
& ~ iFourCheesesTopping("d2")
& ~ iFourCheesesTopping("d1")
& ~ iFourCheesesTopping("d0")
& ~ iFood("d5")
& ~ iFood("d4")
& ~ iFood("d3")
& ~ iFood("d2")
& ~ iFood("d1")
& ~ iFood("d0")
& ~ iFishTopping("d5")
& ~ iFishTopping("d4")
& ~ iFishTopping("d3")
& ~ iFishTopping("d2")
& ~ iFishTopping("d1")
& ~ iFishTopping("d0")
& ~ iFiorentina("d5")
& ~ iFiorentina("d4")
& ~ iFiorentina("d3")
& ~ iFiorentina("d2")
& ~ iFiorentina("d1")
& ~ iFiorentina("d0")
& iDomainConcept("d5")
& iDomainConcept("d4")
& iDomainConcept("d3")
& iDomainConcept("d2")
& ~ iDomainConcept("d1")
& iDomainConcept("d0")
& ~ iDeepPanBase("d5")
& ~ iDeepPanBase("d4")
& ~ iDeepPanBase("d3")
& ~ iDeepPanBase("d2")
& ~ iDeepPanBase("d1")
& ~ iDeepPanBase("d0")
& iCountry("d5")
& iCountry("d4")
& iCountry("d3")
& iCountry("d2")
& ~ iCountry("d1")
& iCountry("d0")
& ~ iChickenTopping("d5")
& ~ iChickenTopping("d4")
& ~ iChickenTopping("d3")
& ~ iChickenTopping("d2")
& ~ iChickenTopping("d1")
& ~ iChickenTopping("d0")
& ~ iCheeseyVegetableTopping("d5")
& ~ iCheeseyVegetableTopping("d4")
& ~ iCheeseyVegetableTopping("d3")
& ~ iCheeseyVegetableTopping("d2")
& ~ iCheeseyVegetableTopping("d1")
& ~ iCheeseyVegetableTopping("d0")
& ~ iCheeseyPizza("d5")
& ~ iCheeseyPizza("d4")
& ~ iCheeseyPizza("d3")
& ~ iCheeseyPizza("d2")
& ~ iCheeseyPizza("d1")
& ~ iCheeseyPizza("d0")
& ~ iCheeseTopping("d5")
& ~ iCheeseTopping("d4")
& ~ iCheeseTopping("d3")
& ~ iCheeseTopping("d2")
& ~ iCheeseTopping("d1")
& ~ iCheeseTopping("d0")
& ~ iCaprina("d5")
& ~ iCaprina("d4")
& ~ iCaprina("d3")
& ~ iCaprina("d2")
& ~ iCaprina("d1")
& ~ iCaprina("d0")
& ~ iCapricciosa("d5")
& ~ iCapricciosa("d4")
& ~ iCapricciosa("d3")
& ~ iCapricciosa("d2")
& ~ iCapricciosa("d1")
& ~ iCapricciosa("d0")
& ~ iCaperTopping("d5")
& ~ iCaperTopping("d4")
& ~ iCaperTopping("d3")
& ~ iCaperTopping("d2")
& ~ iCaperTopping("d1")
& ~ iCaperTopping("d0")
& ~ iCajunSpiceTopping("d5")
& ~ iCajunSpiceTopping("d4")
& ~ iCajunSpiceTopping("d3")
& ~ iCajunSpiceTopping("d2")
& ~ iCajunSpiceTopping("d1")
& ~ iCajunSpiceTopping("d0")
& ~ iCajun("d5")
& ~ iCajun("d4")
& ~ iCajun("d3")
& ~ iCajun("d2")
& ~ iCajun("d1")
& ~ iCajun("d0")
& ~ iAsparagusTopping("d5")
& ~ iAsparagusTopping("d4")
& ~ iAsparagusTopping("d3")
& ~ iAsparagusTopping("d2")
& ~ iAsparagusTopping("d1")
& ~ iAsparagusTopping("d0")
& ~ iArtichokeTopping("d5")
& ~ iArtichokeTopping("d4")
& ~ iArtichokeTopping("d3")
& ~ iArtichokeTopping("d2")
& ~ iArtichokeTopping("d1")
& ~ iArtichokeTopping("d0")
& ~ iAnchoviesTopping("d5")
& ~ iAnchoviesTopping("d4")
& ~ iAnchoviesTopping("d3")
& ~ iAnchoviesTopping("d2")
& ~ iAnchoviesTopping("d1")
& ~ iAnchoviesTopping("d0")
& ~ iAmericanHot("d5")
& ~ iAmericanHot("d4")
& ~ iAmericanHot("d3")
& ~ iAmericanHot("d2")
& ~ iAmericanHot("d1")
& ~ iAmericanHot("d0")
& ~ iAmerican("d5")
& ~ iAmerican("d4")
& ~ iAmerican("d3")
& ~ iAmerican("d2")
& ~ iAmerican("d1")
& ~ iAmerican("d0")
& ~ dataDomain("d5")
& ~ dataDomain("d4")
& ~ dataDomain("d3")
& ~ dataDomain("d2")
& dataDomain("d1")
& ~ dataDomain("d0")
& abstractDomain("d5")
& abstractDomain("d4")
& abstractDomain("d3")
& abstractDomain("d2")
& ~ abstractDomain("d1")
& abstractDomain("d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB036+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : mace4 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/10.38 % Computer : n013.cluster.edu
% 0.09/10.38 % Model : x86_64 x86_64
% 0.09/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.38 % Memory : 8046.5625MB
% 0.09/10.38 % OS : Linux 6.8.0-71-generic
% 0.09/10.38 % CPULimit : 300
% 0.09/10.38 % WCLimit : 300
% 0.09/10.38 % DateTime : Sat Sep 26 11:53:53 UTC 2026
% 0.09/10.38 % CPUTime :
% 0.09/10.39 % Mace4 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/10.39 % Process 2673721 was started by sandbox on n013,
% 0.09/10.39 % Sat Sep 26 11:53:53 2026
% 0.09/10.39 % The command was "/export/starexec/sandbox/solver/bin/mace4 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/10.63
% 0.14/10.63 % SZS status Satisfiable for theBenchmark
% 0.14/10.63 % SZS output start FiniteModel for theBenchmark
% See solution above
%------------------------------------------------------------------------------