%------------------------------------------------------------------------------ % File : Crossbow---0.1 % Problem : SWB036+1 : TPTP v8.1.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : do_Crossbow---0.1 %s % Computer : n032.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Tue Jul 19 18:50:23 EDT 2022 % Result : Satisfiable 5.19s 5.42s % Output : FiniteModel 5.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SWB036+1 : TPTP v8.1.0. Released v5.2.0. % 0.09/0.10 % Command : do_Crossbow---0.1 %s % 0.10/0.29 % Computer : n032.cluster.edu % 0.10/0.29 % Model : x86_64 x86_64 % 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.29 % Memory : 8042.1875MB % 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.29 % CPULimit : 300 % 0.10/0.29 % WCLimit : 600 % 0.10/0.29 % DateTime : Wed Jun 1 12:22:29 EDT 2022 % 0.10/0.29 % CPUTime : % 0.10/0.29 /export/starexec/sandbox/solver/bin % 0.10/0.29 crossbow.opt % 0.10/0.29 do_Crossbow---0.1 % 0.10/0.29 eprover % 0.10/0.29 runsolver % 0.10/0.29 starexec_run_Crossbow---0.1 % 5.19/5.42 % SZS status Satisfiable for theBenchmark.p % 5.19/5.42 % SZS output start FiniteModel for theBenchmark.p % 5.19/5.42 % domain size: 6 % 5.19/5.42 fof(interp, fi_domain, ![X] : (X = 0 | X = 1 | X = 2 | X = 3 | X = 4 | X = 5)). % 5.19/5.42 fof(interp, fi_predicates, abstractDomain(0) & ~abstractDomain(1) & % 5.19/5.42 abstractDomain(2) & % 5.19/5.42 abstractDomain(3) & % 5.19/5.42 abstractDomain(4) & % 5.19/5.42 abstractDomain(5)). % 5.19/5.42 fof(interp, fi_predicates, ~dataDomain(0) & dataDomain(1) & ~dataDomain(2) & % 5.19/5.42 ~dataDomain(3) & % 5.19/5.42 ~dataDomain(4) & % 5.19/5.42 ~dataDomain(5)). % 5.19/5.42 fof(interp, fi_functors, esk100_1(0) = 0 & esk100_1(1) = 0 & esk100_1(2) = 0 & % 5.19/5.42 esk100_1(3) = 0 & % 5.19/5.42 esk100_1(4) = 0 & % 5.19/5.42 esk100_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk101_1(0) = 0 & esk101_1(1) = 0 & esk101_1(2) = 0 & % 5.19/5.42 esk101_1(3) = 0 & % 5.19/5.42 esk101_1(4) = 0 & % 5.19/5.42 esk101_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk102_1(0) = 0 & esk102_1(1) = 0 & esk102_1(2) = 0 & % 5.19/5.42 esk102_1(3) = 0 & % 5.19/5.42 esk102_1(4) = 0 & % 5.19/5.42 esk102_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk103_1(0) = 0 & esk103_1(1) = 0 & esk103_1(2) = 0 & % 5.19/5.42 esk103_1(3) = 0 & % 5.19/5.42 esk103_1(4) = 0 & % 5.19/5.42 esk103_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk104_1(0) = 0 & esk104_1(1) = 0 & esk104_1(2) = 0 & % 5.19/5.42 esk104_1(3) = 0 & % 5.19/5.42 esk104_1(4) = 0 & % 5.19/5.42 esk104_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk105_1(0) = 0 & esk105_1(1) = 0 & esk105_1(2) = 0 & % 5.19/5.42 esk105_1(3) = 0 & % 5.19/5.42 esk105_1(4) = 0 & % 5.19/5.42 esk105_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk106_1(0) = 0 & esk106_1(1) = 0 & esk106_1(2) = 0 & % 5.19/5.42 esk106_1(3) = 0 & % 5.19/5.42 esk106_1(4) = 0 & % 5.19/5.42 esk106_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk107_1(0) = 0 & esk107_1(1) = 0 & esk107_1(2) = 0 & % 5.19/5.42 esk107_1(3) = 0 & % 5.19/5.42 esk107_1(4) = 0 & % 5.19/5.42 esk107_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk108_1(0) = 0 & esk108_1(1) = 0 & esk108_1(2) = 2 & % 5.19/5.42 esk108_1(3) = 0 & % 5.19/5.42 esk108_1(4) = 0 & % 5.19/5.42 esk108_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk109_1(0) = 0 & esk109_1(1) = 0 & esk109_1(2) = 0 & % 5.19/5.42 esk109_1(3) = 0 & % 5.19/5.42 esk109_1(4) = 0 & % 5.19/5.42 esk109_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk10_1(0) = 0 & esk10_1(1) = 0 & esk10_1(2) = 0 & % 5.19/5.42 esk10_1(3) = 0 & % 5.19/5.42 esk10_1(4) = 0 & % 5.19/5.42 esk10_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk110_1(0) = 0 & esk110_1(1) = 0 & esk110_1(2) = 0 & % 5.19/5.42 esk110_1(3) = 0 & % 5.19/5.42 esk110_1(4) = 0 & % 5.19/5.42 esk110_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk111_1(0) = 0 & esk111_1(1) = 0 & esk111_1(2) = 0 & % 5.19/5.42 esk111_1(3) = 0 & % 5.19/5.42 esk111_1(4) = 0 & % 5.19/5.42 esk111_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk112_1(0) = 0 & esk112_1(1) = 0 & esk112_1(2) = 0 & % 5.19/5.42 esk112_1(3) = 0 & % 5.19/5.42 esk112_1(4) = 0 & % 5.19/5.42 esk112_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk113_1(0) = 0 & esk113_1(1) = 0 & esk113_1(2) = 0 & % 5.19/5.42 esk113_1(3) = 0 & % 5.19/5.42 esk113_1(4) = 0 & % 5.19/5.42 esk113_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk114_1(0) = 0 & esk114_1(1) = 0 & esk114_1(2) = 0 & % 5.19/5.42 esk114_1(3) = 0 & % 5.19/5.42 esk114_1(4) = 0 & % 5.19/5.42 esk114_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk115_1(0) = 0 & esk115_1(1) = 0 & esk115_1(2) = 0 & % 5.19/5.42 esk115_1(3) = 0 & % 5.19/5.42 esk115_1(4) = 0 & % 5.19/5.42 esk115_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk116_1(0) = 0 & esk116_1(1) = 0 & esk116_1(2) = 0 & % 5.19/5.42 esk116_1(3) = 0 & % 5.19/5.42 esk116_1(4) = 0 & % 5.19/5.42 esk116_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk117_1(0) = 0 & esk117_1(1) = 0 & esk117_1(2) = 0 & % 5.19/5.42 esk117_1(3) = 0 & % 5.19/5.42 esk117_1(4) = 0 & % 5.19/5.42 esk117_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk118_1(0) = 0 & esk118_1(1) = 0 & esk118_1(2) = 0 & % 5.19/5.42 esk118_1(3) = 0 & % 5.19/5.42 esk118_1(4) = 0 & % 5.19/5.42 esk118_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk119_1(0) = 0 & esk119_1(1) = 0 & esk119_1(2) = 0 & % 5.19/5.42 esk119_1(3) = 0 & % 5.19/5.42 esk119_1(4) = 0 & % 5.19/5.42 esk119_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk11_1(0) = 0 & esk11_1(1) = 0 & esk11_1(2) = 0 & % 5.19/5.42 esk11_1(3) = 0 & % 5.19/5.42 esk11_1(4) = 0 & % 5.19/5.42 esk11_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk120_1(0) = 0 & esk120_1(1) = 0 & esk120_1(2) = 0 & % 5.19/5.42 esk120_1(3) = 0 & % 5.19/5.42 esk120_1(4) = 0 & % 5.19/5.42 esk120_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk121_1(0) = 0 & esk121_1(1) = 0 & esk121_1(2) = 0 & % 5.19/5.42 esk121_1(3) = 0 & % 5.19/5.42 esk121_1(4) = 0 & % 5.19/5.42 esk121_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk122_1(0) = 0 & esk122_1(1) = 0 & esk122_1(2) = 0 & % 5.19/5.42 esk122_1(3) = 0 & % 5.19/5.42 esk122_1(4) = 0 & % 5.19/5.42 esk122_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk123_1(0) = 0 & esk123_1(1) = 0 & esk123_1(2) = 0 & % 5.19/5.42 esk123_1(3) = 0 & % 5.19/5.42 esk123_1(4) = 0 & % 5.19/5.42 esk123_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk124_1(0) = 0 & esk124_1(1) = 0 & esk124_1(2) = 0 & % 5.19/5.42 esk124_1(3) = 0 & % 5.19/5.42 esk124_1(4) = 0 & % 5.19/5.42 esk124_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk125_1(0) = 0 & esk125_1(1) = 0 & esk125_1(2) = 0 & % 5.19/5.42 esk125_1(3) = 0 & % 5.19/5.42 esk125_1(4) = 0 & % 5.19/5.42 esk125_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk126_1(0) = 0 & esk126_1(1) = 0 & esk126_1(2) = 0 & % 5.19/5.42 esk126_1(3) = 0 & % 5.19/5.42 esk126_1(4) = 0 & % 5.19/5.42 esk126_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk127_1(0) = 0 & esk127_1(1) = 0 & esk127_1(2) = 0 & % 5.19/5.42 esk127_1(3) = 0 & % 5.19/5.42 esk127_1(4) = 0 & % 5.19/5.42 esk127_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk128_1(0) = 0 & esk128_1(1) = 0 & esk128_1(2) = 0 & % 5.19/5.42 esk128_1(3) = 0 & % 5.19/5.42 esk128_1(4) = 0 & % 5.19/5.42 esk128_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk129_1(0) = 0 & esk129_1(1) = 0 & esk129_1(2) = 0 & % 5.19/5.42 esk129_1(3) = 0 & % 5.19/5.42 esk129_1(4) = 0 & % 5.19/5.42 esk129_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk12_1(0) = 0 & esk12_1(1) = 0 & esk12_1(2) = 0 & % 5.19/5.42 esk12_1(3) = 0 & % 5.19/5.42 esk12_1(4) = 0 & % 5.19/5.42 esk12_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk130_1(0) = 0 & esk130_1(1) = 0 & esk130_1(2) = 0 & % 5.19/5.42 esk130_1(3) = 0 & % 5.19/5.42 esk130_1(4) = 0 & % 5.19/5.42 esk130_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk131_1(0) = 0 & esk131_1(1) = 0 & esk131_1(2) = 0 & % 5.19/5.42 esk131_1(3) = 0 & % 5.19/5.42 esk131_1(4) = 0 & % 5.19/5.42 esk131_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk132_1(0) = 0 & esk132_1(1) = 0 & esk132_1(2) = 0 & % 5.19/5.42 esk132_1(3) = 0 & % 5.19/5.42 esk132_1(4) = 0 & % 5.19/5.42 esk132_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk133_1(0) = 0 & esk133_1(1) = 0 & esk133_1(2) = 0 & % 5.19/5.42 esk133_1(3) = 0 & % 5.19/5.42 esk133_1(4) = 0 & % 5.19/5.42 esk133_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk134_1(0) = 0 & esk134_1(1) = 0 & esk134_1(2) = 0 & % 5.19/5.42 esk134_1(3) = 0 & % 5.19/5.42 esk134_1(4) = 0 & % 5.19/5.42 esk134_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk135_1(0) = 0 & esk135_1(1) = 0 & esk135_1(2) = 0 & % 5.19/5.42 esk135_1(3) = 0 & % 5.19/5.42 esk135_1(4) = 0 & % 5.19/5.42 esk135_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk136_1(0) = 0 & esk136_1(1) = 0 & esk136_1(2) = 0 & % 5.19/5.42 esk136_1(3) = 0 & % 5.19/5.42 esk136_1(4) = 0 & % 5.19/5.42 esk136_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk137_1(0) = 0 & esk137_1(1) = 0 & esk137_1(2) = 0 & % 5.19/5.42 esk137_1(3) = 0 & % 5.19/5.42 esk137_1(4) = 0 & % 5.19/5.42 esk137_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk138_1(0) = 0 & esk138_1(1) = 0 & esk138_1(2) = 0 & % 5.19/5.42 esk138_1(3) = 0 & % 5.19/5.42 esk138_1(4) = 0 & % 5.19/5.42 esk138_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk139_1(0) = 1 & esk139_1(1) = 0 & esk139_1(2) = 0 & % 5.19/5.42 esk139_1(3) = 0 & % 5.19/5.42 esk139_1(4) = 0 & % 5.19/5.42 esk139_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk13_1(0) = 0 & esk13_1(1) = 0 & esk13_1(2) = 0 & % 5.19/5.42 esk13_1(3) = 0 & % 5.19/5.42 esk13_1(4) = 0 & % 5.19/5.42 esk13_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk140_1(0) = 0 & esk140_1(1) = 0 & esk140_1(2) = 0 & % 5.19/5.42 esk140_1(3) = 0 & % 5.19/5.42 esk140_1(4) = 0 & % 5.19/5.42 esk140_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk141_1(0) = 0 & esk141_1(1) = 0 & esk141_1(2) = 0 & % 5.19/5.42 esk141_1(3) = 0 & % 5.19/5.42 esk141_1(4) = 0 & % 5.19/5.42 esk141_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk142_1(0) = 0 & esk142_1(1) = 0 & esk142_1(2) = 0 & % 5.19/5.42 esk142_1(3) = 0 & % 5.19/5.42 esk142_1(4) = 0 & % 5.19/5.42 esk142_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk143_1(0) = 0 & esk143_1(1) = 0 & esk143_1(2) = 0 & % 5.19/5.42 esk143_1(3) = 0 & % 5.19/5.42 esk143_1(4) = 0 & % 5.19/5.42 esk143_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk144_1(0) = 0 & esk144_1(1) = 0 & esk144_1(2) = 0 & % 5.19/5.42 esk144_1(3) = 0 & % 5.19/5.42 esk144_1(4) = 0 & % 5.19/5.42 esk144_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk145_1(0) = 0 & esk145_1(1) = 0 & esk145_1(2) = 0 & % 5.19/5.42 esk145_1(3) = 0 & % 5.19/5.42 esk145_1(4) = 0 & % 5.19/5.42 esk145_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk146_1(0) = 0 & esk146_1(1) = 0 & esk146_1(2) = 0 & % 5.19/5.42 esk146_1(3) = 0 & % 5.19/5.42 esk146_1(4) = 0 & % 5.19/5.42 esk146_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk147_1(0) = 0 & esk147_1(1) = 0 & esk147_1(2) = 0 & % 5.19/5.42 esk147_1(3) = 0 & % 5.19/5.42 esk147_1(4) = 0 & % 5.19/5.42 esk147_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk148_1(0) = 0 & esk148_1(1) = 0 & esk148_1(2) = 0 & % 5.19/5.42 esk148_1(3) = 0 & % 5.19/5.42 esk148_1(4) = 0 & % 5.19/5.42 esk148_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk149_1(0) = 0 & esk149_1(1) = 0 & esk149_1(2) = 0 & % 5.19/5.42 esk149_1(3) = 0 & % 5.19/5.42 esk149_1(4) = 0 & % 5.19/5.42 esk149_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk14_1(0) = 0 & esk14_1(1) = 0 & esk14_1(2) = 0 & % 5.19/5.42 esk14_1(3) = 0 & % 5.19/5.42 esk14_1(4) = 0 & % 5.19/5.42 esk14_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk150_1(0) = 1 & esk150_1(1) = 0 & esk150_1(2) = 0 & % 5.19/5.42 esk150_1(3) = 0 & % 5.19/5.42 esk150_1(4) = 0 & % 5.19/5.42 esk150_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk151_1(0) = 0 & esk151_1(1) = 0 & esk151_1(2) = 0 & % 5.19/5.42 esk151_1(3) = 0 & % 5.19/5.42 esk151_1(4) = 0 & % 5.19/5.42 esk151_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk152_1(0) = 0 & esk152_1(1) = 0 & esk152_1(2) = 0 & % 5.19/5.42 esk152_1(3) = 0 & % 5.19/5.42 esk152_1(4) = 0 & % 5.19/5.42 esk152_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk153_1(0) = 5 & esk153_1(1) = 5 & esk153_1(2) = 5 & % 5.19/5.42 esk153_1(3) = 5 & % 5.19/5.42 esk153_1(4) = 5 & % 5.19/5.42 esk153_1(5) = 1). % 5.19/5.42 fof(interp, fi_functors, esk154_1(0) = 5 & esk154_1(1) = 5 & esk154_1(2) = 5 & % 5.19/5.42 esk154_1(3) = 5 & % 5.19/5.42 esk154_1(4) = 5 & % 5.19/5.42 esk154_1(5) = 4). % 5.19/5.42 fof(interp, fi_functors, esk155_1(0) = 0 & esk155_1(1) = 0 & esk155_1(2) = 0 & % 5.19/5.42 esk155_1(3) = 0 & % 5.19/5.42 esk155_1(4) = 0 & % 5.19/5.42 esk155_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk156_1(0) = 0 & esk156_1(1) = 0 & esk156_1(2) = 0 & % 5.19/5.42 esk156_1(3) = 0 & % 5.19/5.42 esk156_1(4) = 0 & % 5.19/5.42 esk156_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk157_1(0) = 0 & esk157_1(1) = 0 & esk157_1(2) = 0 & % 5.19/5.42 esk157_1(3) = 0 & % 5.19/5.42 esk157_1(4) = 0 & % 5.19/5.42 esk157_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk158_1(0) = 0 & esk158_1(1) = 0 & esk158_1(2) = 0 & % 5.19/5.42 esk158_1(3) = 0 & % 5.19/5.42 esk158_1(4) = 0 & % 5.19/5.42 esk158_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk159_1(0) = 0 & esk159_1(1) = 1 & esk159_1(2) = 0 & % 5.19/5.42 esk159_1(3) = 0 & % 5.19/5.42 esk159_1(4) = 0 & % 5.19/5.42 esk159_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk15_1(0) = 0 & esk15_1(1) = 0 & esk15_1(2) = 0 & % 5.19/5.42 esk15_1(3) = 0 & % 5.19/5.42 esk15_1(4) = 0 & % 5.19/5.42 esk15_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk160_1(0) = 0 & esk160_1(1) = 0 & esk160_1(2) = 0 & % 5.19/5.42 esk160_1(3) = 0 & % 5.19/5.42 esk160_1(4) = 0 & % 5.19/5.42 esk160_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk161_1(0) = 0 & esk161_1(1) = 0 & esk161_1(2) = 0 & % 5.19/5.42 esk161_1(3) = 0 & % 5.19/5.42 esk161_1(4) = 0 & % 5.19/5.42 esk161_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk162_1(0) = 0 & esk162_1(1) = 0 & esk162_1(2) = 0 & % 5.19/5.42 esk162_1(3) = 0 & % 5.19/5.42 esk162_1(4) = 0 & % 5.19/5.42 esk162_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk163_1(0) = 0 & esk163_1(1) = 0 & esk163_1(2) = 0 & % 5.19/5.42 esk163_1(3) = 0 & % 5.19/5.42 esk163_1(4) = 0 & % 5.19/5.42 esk163_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk16_1(0) = 0 & esk16_1(1) = 0 & esk16_1(2) = 0 & % 5.19/5.42 esk16_1(3) = 0 & % 5.19/5.42 esk16_1(4) = 0 & % 5.19/5.42 esk16_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk17_1(0) = 0 & esk17_1(1) = 0 & esk17_1(2) = 0 & % 5.19/5.42 esk17_1(3) = 0 & % 5.19/5.42 esk17_1(4) = 0 & % 5.19/5.42 esk17_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk18_1(0) = 0 & esk18_1(1) = 2 & esk18_1(2) = 0 & % 5.19/5.42 esk18_1(3) = 0 & % 5.19/5.42 esk18_1(4) = 0 & % 5.19/5.42 esk18_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk19_1(0) = 0 & esk19_1(1) = 0 & esk19_1(2) = 0 & % 5.19/5.42 esk19_1(3) = 0 & % 5.19/5.42 esk19_1(4) = 0 & % 5.19/5.42 esk19_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk1_0 = 0). % 5.19/5.42 fof(interp, fi_functors, esk20_1(0) = 0 & esk20_1(1) = 0 & esk20_1(2) = 0 & % 5.19/5.42 esk20_1(3) = 0 & % 5.19/5.42 esk20_1(4) = 0 & % 5.19/5.42 esk20_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk21_1(0) = 0 & esk21_1(1) = 0 & esk21_1(2) = 0 & % 5.19/5.42 esk21_1(3) = 0 & % 5.19/5.42 esk21_1(4) = 0 & % 5.19/5.42 esk21_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk22_1(0) = 1 & esk22_1(1) = 0 & esk22_1(2) = 0 & % 5.19/5.42 esk22_1(3) = 0 & % 5.19/5.42 esk22_1(4) = 0 & % 5.19/5.42 esk22_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk23_1(0) = 0 & esk23_1(1) = 0 & esk23_1(2) = 0 & % 5.19/5.42 esk23_1(3) = 0 & % 5.19/5.42 esk23_1(4) = 0 & % 5.19/5.42 esk23_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk24_1(0) = 0 & esk24_1(1) = 0 & esk24_1(2) = 0 & % 5.19/5.42 esk24_1(3) = 0 & % 5.19/5.42 esk24_1(4) = 0 & % 5.19/5.42 esk24_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk25_1(0) = 0 & esk25_1(1) = 0 & esk25_1(2) = 0 & % 5.19/5.42 esk25_1(3) = 0 & % 5.19/5.42 esk25_1(4) = 0 & % 5.19/5.42 esk25_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk26_1(0) = 0 & esk26_1(1) = 0 & esk26_1(2) = 0 & % 5.19/5.42 esk26_1(3) = 0 & % 5.19/5.42 esk26_1(4) = 0 & % 5.19/5.42 esk26_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk27_1(0) = 0 & esk27_1(1) = 0 & esk27_1(2) = 0 & % 5.19/5.42 esk27_1(3) = 0 & % 5.19/5.42 esk27_1(4) = 0 & % 5.19/5.42 esk27_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk28_1(0) = 0 & esk28_1(1) = 0 & esk28_1(2) = 0 & % 5.19/5.42 esk28_1(3) = 0 & % 5.19/5.42 esk28_1(4) = 0 & % 5.19/5.42 esk28_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk29_1(0) = 0 & esk29_1(1) = 0 & esk29_1(2) = 0 & % 5.19/5.42 esk29_1(3) = 0 & % 5.19/5.42 esk29_1(4) = 0 & % 5.19/5.42 esk29_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk2_0 = 1). % 5.19/5.42 fof(interp, fi_functors, esk30_1(0) = 0 & esk30_1(1) = 0 & esk30_1(2) = 0 & % 5.19/5.42 esk30_1(3) = 0 & % 5.19/5.42 esk30_1(4) = 0 & % 5.19/5.42 esk30_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk31_1(0) = 0 & esk31_1(1) = 0 & esk31_1(2) = 0 & % 5.19/5.42 esk31_1(3) = 0 & % 5.19/5.42 esk31_1(4) = 0 & % 5.19/5.42 esk31_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk32_1(0) = 0 & esk32_1(1) = 0 & esk32_1(2) = 0 & % 5.19/5.42 esk32_1(3) = 0 & % 5.19/5.42 esk32_1(4) = 0 & % 5.19/5.42 esk32_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk33_1(0) = 0 & esk33_1(1) = 0 & esk33_1(2) = 0 & % 5.19/5.42 esk33_1(3) = 0 & % 5.19/5.42 esk33_1(4) = 0 & % 5.19/5.42 esk33_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk34_1(0) = 0 & esk34_1(1) = 0 & esk34_1(2) = 0 & % 5.19/5.42 esk34_1(3) = 0 & % 5.19/5.42 esk34_1(4) = 0 & % 5.19/5.42 esk34_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk35_1(0) = 0 & esk35_1(1) = 0 & esk35_1(2) = 0 & % 5.19/5.42 esk35_1(3) = 0 & % 5.19/5.42 esk35_1(4) = 0 & % 5.19/5.42 esk35_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk36_1(0) = 0 & esk36_1(1) = 0 & esk36_1(2) = 0 & % 5.19/5.42 esk36_1(3) = 0 & % 5.19/5.42 esk36_1(4) = 0 & % 5.19/5.42 esk36_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk37_1(0) = 1 & esk37_1(1) = 0 & esk37_1(2) = 0 & % 5.19/5.42 esk37_1(3) = 0 & % 5.19/5.42 esk37_1(4) = 0 & % 5.19/5.42 esk37_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk38_1(0) = 0 & esk38_1(1) = 0 & esk38_1(2) = 0 & % 5.19/5.42 esk38_1(3) = 0 & % 5.19/5.42 esk38_1(4) = 0 & % 5.19/5.42 esk38_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk39_1(0) = 0 & esk39_1(1) = 0 & esk39_1(2) = 0 & % 5.19/5.42 esk39_1(3) = 0 & % 5.19/5.42 esk39_1(4) = 0 & % 5.19/5.42 esk39_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk3_1(0) = 0 & esk3_1(1) = 0 & esk3_1(2) = 0 & % 5.19/5.42 esk3_1(3) = 0 & % 5.19/5.42 esk3_1(4) = 0 & % 5.19/5.42 esk3_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk40_1(0) = 0 & esk40_1(1) = 0 & esk40_1(2) = 0 & % 5.19/5.42 esk40_1(3) = 0 & % 5.19/5.42 esk40_1(4) = 0 & % 5.19/5.42 esk40_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk41_1(0) = 0 & esk41_1(1) = 0 & esk41_1(2) = 0 & % 5.19/5.42 esk41_1(3) = 0 & % 5.19/5.42 esk41_1(4) = 0 & % 5.19/5.42 esk41_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk42_1(0) = 0 & esk42_1(1) = 0 & esk42_1(2) = 0 & % 5.19/5.42 esk42_1(3) = 0 & % 5.19/5.42 esk42_1(4) = 0 & % 5.19/5.42 esk42_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk43_1(0) = 0 & esk43_1(1) = 0 & esk43_1(2) = 0 & % 5.19/5.42 esk43_1(3) = 0 & % 5.19/5.42 esk43_1(4) = 0 & % 5.19/5.42 esk43_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk44_1(0) = 1 & esk44_1(1) = 0 & esk44_1(2) = 0 & % 5.19/5.42 esk44_1(3) = 0 & % 5.19/5.42 esk44_1(4) = 0 & % 5.19/5.42 esk44_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk45_1(0) = 0 & esk45_1(1) = 0 & esk45_1(2) = 0 & % 5.19/5.42 esk45_1(3) = 0 & % 5.19/5.42 esk45_1(4) = 0 & % 5.19/5.42 esk45_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk46_1(0) = 0 & esk46_1(1) = 0 & esk46_1(2) = 0 & % 5.19/5.42 esk46_1(3) = 0 & % 5.19/5.42 esk46_1(4) = 0 & % 5.19/5.42 esk46_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk47_1(0) = 0 & esk47_1(1) = 0 & esk47_1(2) = 0 & % 5.19/5.42 esk47_1(3) = 0 & % 5.19/5.42 esk47_1(4) = 0 & % 5.19/5.42 esk47_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk48_1(0) = 0 & esk48_1(1) = 0 & esk48_1(2) = 0 & % 5.19/5.42 esk48_1(3) = 0 & % 5.19/5.42 esk48_1(4) = 0 & % 5.19/5.42 esk48_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk49_1(0) = 0 & esk49_1(1) = 0 & esk49_1(2) = 0 & % 5.19/5.42 esk49_1(3) = 0 & % 5.19/5.42 esk49_1(4) = 0 & % 5.19/5.42 esk49_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk4_1(0) = 0 & esk4_1(1) = 0 & esk4_1(2) = 0 & % 5.19/5.42 esk4_1(3) = 0 & % 5.19/5.42 esk4_1(4) = 0 & % 5.19/5.42 esk4_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk50_1(0) = 0 & esk50_1(1) = 0 & esk50_1(2) = 0 & % 5.19/5.42 esk50_1(3) = 0 & % 5.19/5.42 esk50_1(4) = 0 & % 5.19/5.42 esk50_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk51_1(0) = 0 & esk51_1(1) = 0 & esk51_1(2) = 0 & % 5.19/5.42 esk51_1(3) = 0 & % 5.19/5.42 esk51_1(4) = 0 & % 5.19/5.42 esk51_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk52_1(0) = 0 & esk52_1(1) = 0 & esk52_1(2) = 0 & % 5.19/5.42 esk52_1(3) = 0 & % 5.19/5.42 esk52_1(4) = 0 & % 5.19/5.42 esk52_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk53_1(0) = 0 & esk53_1(1) = 0 & esk53_1(2) = 0 & % 5.19/5.42 esk53_1(3) = 0 & % 5.19/5.42 esk53_1(4) = 0 & % 5.19/5.42 esk53_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk54_1(0) = 0 & esk54_1(1) = 0 & esk54_1(2) = 0 & % 5.19/5.42 esk54_1(3) = 0 & % 5.19/5.42 esk54_1(4) = 0 & % 5.19/5.42 esk54_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk55_1(0) = 1 & esk55_1(1) = 0 & esk55_1(2) = 0 & % 5.19/5.42 esk55_1(3) = 0 & % 5.19/5.42 esk55_1(4) = 0 & % 5.19/5.42 esk55_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk56_1(0) = 0 & esk56_1(1) = 0 & esk56_1(2) = 0 & % 5.19/5.42 esk56_1(3) = 0 & % 5.19/5.42 esk56_1(4) = 0 & % 5.19/5.42 esk56_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk57_1(0) = 0 & esk57_1(1) = 0 & esk57_1(2) = 0 & % 5.19/5.42 esk57_1(3) = 0 & % 5.19/5.42 esk57_1(4) = 0 & % 5.19/5.42 esk57_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk58_1(0) = 0 & esk58_1(1) = 0 & esk58_1(2) = 0 & % 5.19/5.42 esk58_1(3) = 0 & % 5.19/5.42 esk58_1(4) = 0 & % 5.19/5.42 esk58_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk59_1(0) = 0 & esk59_1(1) = 0 & esk59_1(2) = 0 & % 5.19/5.42 esk59_1(3) = 0 & % 5.19/5.42 esk59_1(4) = 0 & % 5.19/5.42 esk59_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk5_1(0) = 0 & esk5_1(1) = 0 & esk5_1(2) = 0 & % 5.19/5.42 esk5_1(3) = 0 & % 5.19/5.42 esk5_1(4) = 0 & % 5.19/5.42 esk5_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk60_1(0) = 0 & esk60_1(1) = 0 & esk60_1(2) = 0 & % 5.19/5.42 esk60_1(3) = 0 & % 5.19/5.42 esk60_1(4) = 0 & % 5.19/5.42 esk60_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk61_1(0) = 0 & esk61_1(1) = 0 & esk61_1(2) = 0 & % 5.19/5.42 esk61_1(3) = 0 & % 5.19/5.42 esk61_1(4) = 0 & % 5.19/5.42 esk61_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk62_1(0) = 0 & esk62_1(1) = 3 & esk62_1(2) = 0 & % 5.19/5.42 esk62_1(3) = 0 & % 5.19/5.42 esk62_1(4) = 0 & % 5.19/5.42 esk62_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk63_1(0) = 0 & esk63_1(1) = 0 & esk63_1(2) = 0 & % 5.19/5.42 esk63_1(3) = 0 & % 5.19/5.42 esk63_1(4) = 0 & % 5.19/5.42 esk63_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk64_1(0) = 0 & esk64_1(1) = 0 & esk64_1(2) = 0 & % 5.19/5.42 esk64_1(3) = 0 & % 5.19/5.42 esk64_1(4) = 0 & % 5.19/5.42 esk64_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk65_1(0) = 0 & esk65_1(1) = 0 & esk65_1(2) = 0 & % 5.19/5.42 esk65_1(3) = 0 & % 5.19/5.42 esk65_1(4) = 0 & % 5.19/5.42 esk65_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk66_1(0) = 0 & esk66_1(1) = 0 & esk66_1(2) = 0 & % 5.19/5.42 esk66_1(3) = 0 & % 5.19/5.42 esk66_1(4) = 0 & % 5.19/5.42 esk66_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk67_1(0) = 0 & esk67_1(1) = 0 & esk67_1(2) = 0 & % 5.19/5.42 esk67_1(3) = 0 & % 5.19/5.42 esk67_1(4) = 0 & % 5.19/5.42 esk67_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk68_1(0) = 0 & esk68_1(1) = 0 & esk68_1(2) = 0 & % 5.19/5.42 esk68_1(3) = 0 & % 5.19/5.42 esk68_1(4) = 0 & % 5.19/5.42 esk68_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk69_1(0) = 0 & esk69_1(1) = 0 & esk69_1(2) = 0 & % 5.19/5.42 esk69_1(3) = 0 & % 5.19/5.42 esk69_1(4) = 0 & % 5.19/5.42 esk69_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk6_1(0) = 0 & esk6_1(1) = 0 & esk6_1(2) = 0 & % 5.19/5.42 esk6_1(3) = 0 & % 5.19/5.42 esk6_1(4) = 0 & % 5.19/5.42 esk6_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk70_1(0) = 0 & esk70_1(1) = 0 & esk70_1(2) = 0 & % 5.19/5.42 esk70_1(3) = 0 & % 5.19/5.42 esk70_1(4) = 0 & % 5.19/5.42 esk70_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk71_1(0) = 0 & esk71_1(1) = 0 & esk71_1(2) = 0 & % 5.19/5.42 esk71_1(3) = 0 & % 5.19/5.42 esk71_1(4) = 0 & % 5.19/5.42 esk71_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk72_1(0) = 0 & esk72_1(1) = 0 & esk72_1(2) = 0 & % 5.19/5.42 esk72_1(3) = 0 & % 5.19/5.42 esk72_1(4) = 0 & % 5.19/5.42 esk72_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk73_1(0) = 0 & esk73_1(1) = 0 & esk73_1(2) = 0 & % 5.19/5.42 esk73_1(3) = 0 & % 5.19/5.42 esk73_1(4) = 0 & % 5.19/5.42 esk73_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk74_1(0) = 0 & esk74_1(1) = 0 & esk74_1(2) = 0 & % 5.19/5.42 esk74_1(3) = 0 & % 5.19/5.42 esk74_1(4) = 0 & % 5.19/5.42 esk74_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk75_1(0) = 0 & esk75_1(1) = 0 & esk75_1(2) = 0 & % 5.19/5.42 esk75_1(3) = 0 & % 5.19/5.42 esk75_1(4) = 0 & % 5.19/5.42 esk75_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk76_1(0) = 0 & esk76_1(1) = 0 & esk76_1(2) = 0 & % 5.19/5.42 esk76_1(3) = 0 & % 5.19/5.42 esk76_1(4) = 0 & % 5.19/5.42 esk76_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk77_1(0) = 0 & esk77_1(1) = 0 & esk77_1(2) = 0 & % 5.19/5.42 esk77_1(3) = 0 & % 5.19/5.42 esk77_1(4) = 0 & % 5.19/5.42 esk77_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk78_1(0) = 0 & esk78_1(1) = 0 & esk78_1(2) = 0 & % 5.19/5.42 esk78_1(3) = 0 & % 5.19/5.42 esk78_1(4) = 0 & % 5.19/5.42 esk78_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk79_1(0) = 0 & esk79_1(1) = 0 & esk79_1(2) = 0 & % 5.19/5.42 esk79_1(3) = 0 & % 5.19/5.42 esk79_1(4) = 0 & % 5.19/5.42 esk79_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk7_1(0) = 0 & esk7_1(1) = 0 & esk7_1(2) = 0 & % 5.19/5.42 esk7_1(3) = 0 & % 5.19/5.42 esk7_1(4) = 0 & % 5.19/5.42 esk7_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk80_1(0) = 0 & esk80_1(1) = 0 & esk80_1(2) = 0 & % 5.19/5.42 esk80_1(3) = 0 & % 5.19/5.42 esk80_1(4) = 0 & % 5.19/5.42 esk80_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk81_1(0) = 0 & esk81_1(1) = 0 & esk81_1(2) = 0 & % 5.19/5.42 esk81_1(3) = 0 & % 5.19/5.42 esk81_1(4) = 0 & % 5.19/5.42 esk81_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk82_1(0) = 0 & esk82_1(1) = 0 & esk82_1(2) = 0 & % 5.19/5.42 esk82_1(3) = 0 & % 5.19/5.42 esk82_1(4) = 0 & % 5.19/5.42 esk82_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk83_1(0) = 0 & esk83_1(1) = 0 & esk83_1(2) = 0 & % 5.19/5.42 esk83_1(3) = 0 & % 5.19/5.42 esk83_1(4) = 0 & % 5.19/5.42 esk83_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk84_1(0) = 0 & esk84_1(1) = 0 & esk84_1(2) = 0 & % 5.19/5.42 esk84_1(3) = 0 & % 5.19/5.42 esk84_1(4) = 0 & % 5.19/5.42 esk84_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk85_1(0) = 1 & esk85_1(1) = 0 & esk85_1(2) = 0 & % 5.19/5.42 esk85_1(3) = 0 & % 5.19/5.42 esk85_1(4) = 0 & % 5.19/5.42 esk85_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk86_1(0) = 0 & esk86_1(1) = 0 & esk86_1(2) = 0 & % 5.19/5.42 esk86_1(3) = 0 & % 5.19/5.42 esk86_1(4) = 0 & % 5.19/5.42 esk86_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk87_1(0) = 0 & esk87_1(1) = 0 & esk87_1(2) = 0 & % 5.19/5.42 esk87_1(3) = 0 & % 5.19/5.42 esk87_1(4) = 0 & % 5.19/5.42 esk87_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk88_1(0) = 0 & esk88_1(1) = 0 & esk88_1(2) = 0 & % 5.19/5.42 esk88_1(3) = 0 & % 5.19/5.42 esk88_1(4) = 0 & % 5.19/5.42 esk88_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk89_1(0) = 0 & esk89_1(1) = 0 & esk89_1(2) = 0 & % 5.19/5.42 esk89_1(3) = 0 & % 5.19/5.42 esk89_1(4) = 0 & % 5.19/5.42 esk89_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk8_1(0) = 0 & esk8_1(1) = 0 & esk8_1(2) = 0 & % 5.19/5.42 esk8_1(3) = 0 & % 5.19/5.42 esk8_1(4) = 0 & % 5.19/5.42 esk8_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk90_1(0) = 0 & esk90_1(1) = 0 & esk90_1(2) = 0 & % 5.19/5.42 esk90_1(3) = 0 & % 5.19/5.42 esk90_1(4) = 0 & % 5.19/5.42 esk90_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk91_1(0) = 0 & esk91_1(1) = 0 & esk91_1(2) = 0 & % 5.19/5.42 esk91_1(3) = 0 & % 5.19/5.42 esk91_1(4) = 0 & % 5.19/5.42 esk91_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk92_1(0) = 0 & esk92_1(1) = 0 & esk92_1(2) = 0 & % 5.19/5.42 esk92_1(3) = 0 & % 5.19/5.42 esk92_1(4) = 0 & % 5.19/5.42 esk92_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk93_1(0) = 0 & esk93_1(1) = 0 & esk93_1(2) = 0 & % 5.19/5.42 esk93_1(3) = 0 & % 5.19/5.42 esk93_1(4) = 0 & % 5.19/5.42 esk93_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk94_1(0) = 0 & esk94_1(1) = 0 & esk94_1(2) = 0 & % 5.19/5.42 esk94_1(3) = 0 & % 5.19/5.42 esk94_1(4) = 0 & % 5.19/5.42 esk94_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk95_1(0) = 0 & esk95_1(1) = 0 & esk95_1(2) = 0 & % 5.19/5.42 esk95_1(3) = 0 & % 5.19/5.42 esk95_1(4) = 0 & % 5.19/5.42 esk95_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk96_1(0) = 0 & esk96_1(1) = 0 & esk96_1(2) = 0 & % 5.19/5.42 esk96_1(3) = 0 & % 5.19/5.42 esk96_1(4) = 0 & % 5.19/5.42 esk96_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk97_1(0) = 0 & esk97_1(1) = 0 & esk97_1(2) = 0 & % 5.19/5.42 esk97_1(3) = 0 & % 5.19/5.42 esk97_1(4) = 0 & % 5.19/5.42 esk97_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk98_1(0) = 0 & esk98_1(1) = 0 & esk98_1(2) = 0 & % 5.19/5.42 esk98_1(3) = 0 & % 5.19/5.42 esk98_1(4) = 0 & % 5.19/5.42 esk98_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk99_1(0) = 0 & esk99_1(1) = 0 & esk99_1(2) = 0 & % 5.19/5.42 esk99_1(3) = 0 & % 5.19/5.42 esk99_1(4) = 0 & % 5.19/5.42 esk99_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, esk9_1(0) = 0 & esk9_1(1) = 0 & esk9_1(2) = 0 & % 5.19/5.42 esk9_1(3) = 0 & % 5.19/5.42 esk9_1(4) = 0 & % 5.19/5.42 esk9_1(5) = 0). % 5.19/5.42 fof(interp, fi_functors, iAmerica = 2). % 5.19/5.42 fof(interp, fi_predicates, ~iAmerican(0) & ~iAmerican(1) & ~iAmerican(2) & % 5.19/5.42 ~iAmerican(3) & % 5.19/5.42 ~iAmerican(4) & % 5.19/5.42 ~iAmerican(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iAmericanHot(0) & ~iAmericanHot(1) & % 5.19/5.42 ~iAmericanHot(2) & % 5.19/5.42 ~iAmericanHot(3) & % 5.19/5.42 ~iAmericanHot(4) & % 5.19/5.42 ~iAmericanHot(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iAnchoviesTopping(0) & ~iAnchoviesTopping(1) & % 5.19/5.42 ~iAnchoviesTopping(2) & % 5.19/5.42 ~iAnchoviesTopping(3) & % 5.19/5.42 ~iAnchoviesTopping(4) & % 5.19/5.42 ~iAnchoviesTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iArtichokeTopping(0) & ~iArtichokeTopping(1) & % 5.19/5.42 ~iArtichokeTopping(2) & % 5.19/5.42 ~iArtichokeTopping(3) & % 5.19/5.42 ~iArtichokeTopping(4) & % 5.19/5.42 ~iArtichokeTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iAsparagusTopping(0) & ~iAsparagusTopping(1) & % 5.19/5.42 ~iAsparagusTopping(2) & % 5.19/5.42 ~iAsparagusTopping(3) & % 5.19/5.42 ~iAsparagusTopping(4) & % 5.19/5.42 ~iAsparagusTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iCajun(0) & ~iCajun(1) & ~iCajun(2) & ~iCajun(3) & % 5.19/5.42 ~iCajun(4) & % 5.19/5.42 ~iCajun(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iCajunSpiceTopping(0) & ~iCajunSpiceTopping(1) & % 5.19/5.42 ~iCajunSpiceTopping(2) & % 5.19/5.42 ~iCajunSpiceTopping(3) & % 5.19/5.42 ~iCajunSpiceTopping(4) & % 5.19/5.42 ~iCajunSpiceTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iCaperTopping(0) & ~iCaperTopping(1) & % 5.19/5.42 ~iCaperTopping(2) & % 5.19/5.42 ~iCaperTopping(3) & % 5.19/5.42 ~iCaperTopping(4) & % 5.19/5.42 ~iCaperTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iCapricciosa(0) & ~iCapricciosa(1) & % 5.19/5.42 ~iCapricciosa(2) & % 5.19/5.42 ~iCapricciosa(3) & % 5.19/5.42 ~iCapricciosa(4) & % 5.19/5.42 ~iCapricciosa(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iCaprina(0) & ~iCaprina(1) & ~iCaprina(2) & % 5.19/5.42 ~iCaprina(3) & % 5.19/5.42 ~iCaprina(4) & % 5.19/5.42 ~iCaprina(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iCheeseTopping(0) & ~iCheeseTopping(1) & % 5.19/5.42 ~iCheeseTopping(2) & % 5.19/5.42 ~iCheeseTopping(3) & % 5.19/5.42 ~iCheeseTopping(4) & % 5.19/5.42 ~iCheeseTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iCheeseyPizza(0) & ~iCheeseyPizza(1) & % 5.19/5.42 ~iCheeseyPizza(2) & % 5.19/5.42 ~iCheeseyPizza(3) & % 5.19/5.42 ~iCheeseyPizza(4) & % 5.19/5.42 ~iCheeseyPizza(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iCheeseyVegetableTopping(0) & % 5.19/5.42 ~iCheeseyVegetableTopping(1) & % 5.19/5.42 ~iCheeseyVegetableTopping(2) & % 5.19/5.42 ~iCheeseyVegetableTopping(3) & % 5.19/5.42 ~iCheeseyVegetableTopping(4) & % 5.19/5.42 ~iCheeseyVegetableTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iChickenTopping(0) & ~iChickenTopping(1) & % 5.19/5.42 ~iChickenTopping(2) & % 5.19/5.42 ~iChickenTopping(3) & % 5.19/5.42 ~iChickenTopping(4) & % 5.19/5.42 ~iChickenTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, iCountry(0) & ~iCountry(1) & iCountry(2) & % 5.19/5.42 iCountry(3) & % 5.19/5.42 iCountry(4) & % 5.19/5.42 iCountry(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iDeepPanBase(0) & ~iDeepPanBase(1) & % 5.19/5.42 ~iDeepPanBase(2) & % 5.19/5.42 ~iDeepPanBase(3) & % 5.19/5.42 ~iDeepPanBase(4) & % 5.19/5.42 ~iDeepPanBase(5)). % 5.19/5.42 fof(interp, fi_predicates, iDomainConcept(0) & ~iDomainConcept(1) & % 5.19/5.42 iDomainConcept(2) & % 5.19/5.42 iDomainConcept(3) & % 5.19/5.42 iDomainConcept(4) & % 5.19/5.42 iDomainConcept(5)). % 5.19/5.42 fof(interp, fi_functors, iEngland = 5). % 5.19/5.42 fof(interp, fi_predicates, ~iFiorentina(0) & ~iFiorentina(1) & ~iFiorentina(2) & % 5.19/5.42 ~iFiorentina(3) & % 5.19/5.42 ~iFiorentina(4) & % 5.19/5.42 ~iFiorentina(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iFishTopping(0) & ~iFishTopping(1) & % 5.19/5.42 ~iFishTopping(2) & % 5.19/5.42 ~iFishTopping(3) & % 5.19/5.42 ~iFishTopping(4) & % 5.19/5.42 ~iFishTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iFood(0) & ~iFood(1) & ~iFood(2) & ~iFood(3) & % 5.19/5.42 ~iFood(4) & % 5.19/5.42 ~iFood(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iFourCheesesTopping(0) & ~iFourCheesesTopping(1) & % 5.19/5.42 ~iFourCheesesTopping(2) & % 5.19/5.42 ~iFourCheesesTopping(3) & % 5.19/5.42 ~iFourCheesesTopping(4) & % 5.19/5.42 ~iFourCheesesTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iFourSeasons(0) & ~iFourSeasons(1) & % 5.19/5.42 ~iFourSeasons(2) & % 5.19/5.42 ~iFourSeasons(3) & % 5.19/5.42 ~iFourSeasons(4) & % 5.19/5.42 ~iFourSeasons(5)). % 5.19/5.42 fof(interp, fi_functors, iFrance = 3). % 5.19/5.42 fof(interp, fi_predicates, ~iFruitTopping(0) & ~iFruitTopping(1) & % 5.19/5.42 ~iFruitTopping(2) & % 5.19/5.42 ~iFruitTopping(3) & % 5.19/5.42 ~iFruitTopping(4) & % 5.19/5.42 ~iFruitTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iFruttiDiMare(0) & ~iFruttiDiMare(1) & % 5.19/5.42 ~iFruttiDiMare(2) & % 5.19/5.42 ~iFruttiDiMare(3) & % 5.19/5.42 ~iFruttiDiMare(4) & % 5.19/5.42 ~iFruttiDiMare(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iGarlicTopping(0) & ~iGarlicTopping(1) & % 5.19/5.42 ~iGarlicTopping(2) & % 5.19/5.42 ~iGarlicTopping(3) & % 5.19/5.42 ~iGarlicTopping(4) & % 5.19/5.42 ~iGarlicTopping(5)). % 5.19/5.42 fof(interp, fi_functors, iGermany = 4). % 5.19/5.42 fof(interp, fi_predicates, ~iGiardiniera(0) & ~iGiardiniera(1) & % 5.19/5.42 ~iGiardiniera(2) & % 5.19/5.42 ~iGiardiniera(3) & % 5.19/5.42 ~iGiardiniera(4) & % 5.19/5.42 ~iGiardiniera(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iGoatsCheeseTopping(0) & ~iGoatsCheeseTopping(1) & % 5.19/5.42 ~iGoatsCheeseTopping(2) & % 5.19/5.42 ~iGoatsCheeseTopping(3) & % 5.19/5.42 ~iGoatsCheeseTopping(4) & % 5.19/5.42 ~iGoatsCheeseTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iGorgonzolaTopping(0) & ~iGorgonzolaTopping(1) & % 5.19/5.42 ~iGorgonzolaTopping(2) & % 5.19/5.42 ~iGorgonzolaTopping(3) & % 5.19/5.42 ~iGorgonzolaTopping(4) & % 5.19/5.42 ~iGorgonzolaTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iGreenPepperTopping(0) & ~iGreenPepperTopping(1) & % 5.19/5.42 ~iGreenPepperTopping(2) & % 5.19/5.42 ~iGreenPepperTopping(3) & % 5.19/5.42 ~iGreenPepperTopping(4) & % 5.19/5.42 ~iGreenPepperTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iHamTopping(0) & ~iHamTopping(1) & ~iHamTopping(2) & % 5.19/5.42 ~iHamTopping(3) & % 5.19/5.42 ~iHamTopping(4) & % 5.19/5.42 ~iHamTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iHerbSpiceTopping(0) & ~iHerbSpiceTopping(1) & % 5.19/5.42 ~iHerbSpiceTopping(2) & % 5.19/5.42 ~iHerbSpiceTopping(3) & % 5.19/5.42 ~iHerbSpiceTopping(4) & % 5.19/5.42 ~iHerbSpiceTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iHot(0) & ~iHot(1) & ~iHot(2) & ~iHot(3) & ~iHot(4) & % 5.19/5.42 ~iHot(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iHotGreenPepperTopping(0) & % 5.19/5.42 ~iHotGreenPepperTopping(1) & % 5.19/5.42 ~iHotGreenPepperTopping(2) & % 5.19/5.42 ~iHotGreenPepperTopping(3) & % 5.19/5.42 ~iHotGreenPepperTopping(4) & % 5.19/5.42 ~iHotGreenPepperTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iHotSpicedBeefTopping(0) & ~iHotSpicedBeefTopping(1) & % 5.19/5.42 ~iHotSpicedBeefTopping(2) & % 5.19/5.42 ~iHotSpicedBeefTopping(3) & % 5.19/5.42 ~iHotSpicedBeefTopping(4) & % 5.19/5.42 ~iHotSpicedBeefTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iIceCream(0) & ~iIceCream(1) & ~iIceCream(2) & % 5.19/5.42 ~iIceCream(3) & % 5.19/5.42 ~iIceCream(4) & % 5.19/5.42 ~iIceCream(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iInterestingPizza(0) & ~iInterestingPizza(1) & % 5.19/5.42 ~iInterestingPizza(2) & % 5.19/5.42 ~iInterestingPizza(3) & % 5.19/5.42 ~iInterestingPizza(4) & % 5.19/5.42 ~iInterestingPizza(5)). % 5.19/5.42 fof(interp, fi_functors, iItaly = 0). % 5.19/5.42 fof(interp, fi_predicates, ~iJalapenoPepperTopping(0) & % 5.19/5.42 ~iJalapenoPepperTopping(1) & % 5.19/5.42 ~iJalapenoPepperTopping(2) & % 5.19/5.42 ~iJalapenoPepperTopping(3) & % 5.19/5.42 ~iJalapenoPepperTopping(4) & % 5.19/5.42 ~iJalapenoPepperTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iLaReine(0) & ~iLaReine(1) & ~iLaReine(2) & % 5.19/5.42 ~iLaReine(3) & % 5.19/5.42 ~iLaReine(4) & % 5.19/5.42 ~iLaReine(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iLeekTopping(0) & ~iLeekTopping(1) & % 5.19/5.42 ~iLeekTopping(2) & % 5.19/5.42 ~iLeekTopping(3) & % 5.19/5.42 ~iLeekTopping(4) & % 5.19/5.42 ~iLeekTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iMargherita(0) & ~iMargherita(1) & ~iMargherita(2) & % 5.19/5.42 ~iMargherita(3) & % 5.19/5.42 ~iMargherita(4) & % 5.19/5.42 ~iMargherita(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iMeatTopping(0) & ~iMeatTopping(1) & % 5.19/5.42 ~iMeatTopping(2) & % 5.19/5.42 ~iMeatTopping(3) & % 5.19/5.42 ~iMeatTopping(4) & % 5.19/5.42 ~iMeatTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iMeatyPizza(0) & ~iMeatyPizza(1) & ~iMeatyPizza(2) & % 5.19/5.42 ~iMeatyPizza(3) & % 5.19/5.42 ~iMeatyPizza(4) & % 5.19/5.42 ~iMeatyPizza(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iMedium(0) & ~iMedium(1) & ~iMedium(2) & ~iMedium(3) & % 5.19/5.42 ~iMedium(4) & % 5.19/5.42 ~iMedium(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iMild(0) & ~iMild(1) & ~iMild(2) & ~iMild(3) & % 5.19/5.42 ~iMild(4) & % 5.19/5.42 ~iMild(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iMixedSeafoodTopping(0) & ~iMixedSeafoodTopping(1) & % 5.19/5.42 ~iMixedSeafoodTopping(2) & % 5.19/5.42 ~iMixedSeafoodTopping(3) & % 5.19/5.42 ~iMixedSeafoodTopping(4) & % 5.19/5.42 ~iMixedSeafoodTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iMozzarellaTopping(0) & ~iMozzarellaTopping(1) & % 5.19/5.42 ~iMozzarellaTopping(2) & % 5.19/5.42 ~iMozzarellaTopping(3) & % 5.19/5.42 ~iMozzarellaTopping(4) & % 5.19/5.42 ~iMozzarellaTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iMushroom(0) & ~iMushroom(1) & ~iMushroom(2) & % 5.19/5.42 ~iMushroom(3) & % 5.19/5.42 ~iMushroom(4) & % 5.19/5.42 ~iMushroom(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iMushroomTopping(0) & ~iMushroomTopping(1) & % 5.19/5.42 ~iMushroomTopping(2) & % 5.19/5.42 ~iMushroomTopping(3) & % 5.19/5.42 ~iMushroomTopping(4) & % 5.19/5.42 ~iMushroomTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iNamedPizza(0) & ~iNamedPizza(1) & ~iNamedPizza(2) & % 5.19/5.42 ~iNamedPizza(3) & % 5.19/5.42 ~iNamedPizza(4) & % 5.19/5.42 ~iNamedPizza(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iNapoletana(0) & ~iNapoletana(1) & ~iNapoletana(2) & % 5.19/5.42 ~iNapoletana(3) & % 5.19/5.42 ~iNapoletana(4) & % 5.19/5.42 ~iNapoletana(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iNonVegetarianPizza(0) & ~iNonVegetarianPizza(1) & % 5.19/5.42 ~iNonVegetarianPizza(2) & % 5.19/5.42 ~iNonVegetarianPizza(3) & % 5.19/5.42 ~iNonVegetarianPizza(4) & % 5.19/5.42 ~iNonVegetarianPizza(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iNutTopping(0) & ~iNutTopping(1) & ~iNutTopping(2) & % 5.19/5.42 ~iNutTopping(3) & % 5.19/5.42 ~iNutTopping(4) & % 5.19/5.42 ~iNutTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iOliveTopping(0) & ~iOliveTopping(1) & % 5.19/5.42 ~iOliveTopping(2) & % 5.19/5.42 ~iOliveTopping(3) & % 5.19/5.42 ~iOliveTopping(4) & % 5.19/5.42 ~iOliveTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iOnionTopping(0) & ~iOnionTopping(1) & % 5.19/5.42 ~iOnionTopping(2) & % 5.19/5.42 ~iOnionTopping(3) & % 5.19/5.42 ~iOnionTopping(4) & % 5.19/5.42 ~iOnionTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iParmaHamTopping(0) & ~iParmaHamTopping(1) & % 5.19/5.42 ~iParmaHamTopping(2) & % 5.19/5.42 ~iParmaHamTopping(3) & % 5.19/5.42 ~iParmaHamTopping(4) & % 5.19/5.42 ~iParmaHamTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iParmense(0) & ~iParmense(1) & ~iParmense(2) & % 5.19/5.42 ~iParmense(3) & % 5.19/5.42 ~iParmense(4) & % 5.19/5.42 ~iParmense(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iParmesanTopping(0) & ~iParmesanTopping(1) & % 5.19/5.42 ~iParmesanTopping(2) & % 5.19/5.42 ~iParmesanTopping(3) & % 5.19/5.42 ~iParmesanTopping(4) & % 5.19/5.42 ~iParmesanTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iPeperonataTopping(0) & ~iPeperonataTopping(1) & % 5.19/5.42 ~iPeperonataTopping(2) & % 5.19/5.42 ~iPeperonataTopping(3) & % 5.19/5.42 ~iPeperonataTopping(4) & % 5.19/5.42 ~iPeperonataTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iPeperoniSausageTopping(0) & % 5.19/5.42 ~iPeperoniSausageTopping(1) & % 5.19/5.42 ~iPeperoniSausageTopping(2) & % 5.19/5.42 ~iPeperoniSausageTopping(3) & % 5.19/5.42 ~iPeperoniSausageTopping(4) & % 5.19/5.42 ~iPeperoniSausageTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iPepperTopping(0) & ~iPepperTopping(1) & % 5.19/5.42 ~iPepperTopping(2) & % 5.19/5.42 ~iPepperTopping(3) & % 5.19/5.42 ~iPepperTopping(4) & % 5.19/5.42 ~iPepperTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iPetitPoisTopping(0) & ~iPetitPoisTopping(1) & % 5.19/5.42 ~iPetitPoisTopping(2) & % 5.19/5.42 ~iPetitPoisTopping(3) & % 5.19/5.42 ~iPetitPoisTopping(4) & % 5.19/5.42 ~iPetitPoisTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iPineKernels(0) & ~iPineKernels(1) & % 5.19/5.42 ~iPineKernels(2) & % 5.19/5.42 ~iPineKernels(3) & % 5.19/5.42 ~iPineKernels(4) & % 5.19/5.42 ~iPineKernels(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iPizza(0) & ~iPizza(1) & ~iPizza(2) & ~iPizza(3) & % 5.19/5.42 ~iPizza(4) & % 5.19/5.42 ~iPizza(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iPizzaBase(0) & ~iPizzaBase(1) & ~iPizzaBase(2) & % 5.19/5.42 ~iPizzaBase(3) & % 5.19/5.42 ~iPizzaBase(4) & % 5.19/5.42 ~iPizzaBase(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iPizzaTopping(0) & ~iPizzaTopping(1) & % 5.19/5.42 ~iPizzaTopping(2) & % 5.19/5.42 ~iPizzaTopping(3) & % 5.19/5.42 ~iPizzaTopping(4) & % 5.19/5.42 ~iPizzaTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iPolloAdAstra(0) & ~iPolloAdAstra(1) & % 5.19/5.42 ~iPolloAdAstra(2) & % 5.19/5.42 ~iPolloAdAstra(3) & % 5.19/5.42 ~iPolloAdAstra(4) & % 5.19/5.42 ~iPolloAdAstra(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iPrawnsTopping(0) & ~iPrawnsTopping(1) & % 5.19/5.42 ~iPrawnsTopping(2) & % 5.19/5.42 ~iPrawnsTopping(3) & % 5.19/5.42 ~iPrawnsTopping(4) & % 5.19/5.42 ~iPrawnsTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iPrinceCarlo(0) & ~iPrinceCarlo(1) & % 5.19/5.42 ~iPrinceCarlo(2) & % 5.19/5.42 ~iPrinceCarlo(3) & % 5.19/5.42 ~iPrinceCarlo(4) & % 5.19/5.42 ~iPrinceCarlo(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iQuattroFormaggi(0) & ~iQuattroFormaggi(1) & % 5.19/5.42 ~iQuattroFormaggi(2) & % 5.19/5.42 ~iQuattroFormaggi(3) & % 5.19/5.42 ~iQuattroFormaggi(4) & % 5.19/5.42 ~iQuattroFormaggi(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iRealItalianPizza(0) & ~iRealItalianPizza(1) & % 5.19/5.42 ~iRealItalianPizza(2) & % 5.19/5.42 ~iRealItalianPizza(3) & % 5.19/5.42 ~iRealItalianPizza(4) & % 5.19/5.42 ~iRealItalianPizza(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iRedOnionTopping(0) & ~iRedOnionTopping(1) & % 5.19/5.42 ~iRedOnionTopping(2) & % 5.19/5.42 ~iRedOnionTopping(3) & % 5.19/5.42 ~iRedOnionTopping(4) & % 5.19/5.42 ~iRedOnionTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iRocketTopping(0) & ~iRocketTopping(1) & % 5.19/5.42 ~iRocketTopping(2) & % 5.19/5.42 ~iRocketTopping(3) & % 5.19/5.42 ~iRocketTopping(4) & % 5.19/5.42 ~iRocketTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iRosa(0) & ~iRosa(1) & ~iRosa(2) & ~iRosa(3) & % 5.19/5.42 ~iRosa(4) & % 5.19/5.42 ~iRosa(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iRosemaryTopping(0) & ~iRosemaryTopping(1) & % 5.19/5.42 ~iRosemaryTopping(2) & % 5.19/5.42 ~iRosemaryTopping(3) & % 5.19/5.42 ~iRosemaryTopping(4) & % 5.19/5.42 ~iRosemaryTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iSauceTopping(0) & ~iSauceTopping(1) & % 5.19/5.42 ~iSauceTopping(2) & % 5.19/5.42 ~iSauceTopping(3) & % 5.19/5.42 ~iSauceTopping(4) & % 5.19/5.42 ~iSauceTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iSiciliana(0) & ~iSiciliana(1) & ~iSiciliana(2) & % 5.19/5.42 ~iSiciliana(3) & % 5.19/5.42 ~iSiciliana(4) & % 5.19/5.42 ~iSiciliana(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iSlicedTomatoTopping(0) & ~iSlicedTomatoTopping(1) & % 5.19/5.42 ~iSlicedTomatoTopping(2) & % 5.19/5.42 ~iSlicedTomatoTopping(3) & % 5.19/5.42 ~iSlicedTomatoTopping(4) & % 5.19/5.42 ~iSlicedTomatoTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iSloppyGiuseppe(0) & ~iSloppyGiuseppe(1) & % 5.19/5.42 ~iSloppyGiuseppe(2) & % 5.19/5.42 ~iSloppyGiuseppe(3) & % 5.19/5.42 ~iSloppyGiuseppe(4) & % 5.19/5.42 ~iSloppyGiuseppe(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iSoho(0) & ~iSoho(1) & ~iSoho(2) & ~iSoho(3) & % 5.19/5.42 ~iSoho(4) & % 5.19/5.42 ~iSoho(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iSpiciness(0) & ~iSpiciness(1) & ~iSpiciness(2) & % 5.19/5.42 ~iSpiciness(3) & % 5.19/5.42 ~iSpiciness(4) & % 5.19/5.42 ~iSpiciness(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iSpicyPizza(0) & ~iSpicyPizza(1) & ~iSpicyPizza(2) & % 5.19/5.42 ~iSpicyPizza(3) & % 5.19/5.42 ~iSpicyPizza(4) & % 5.19/5.42 ~iSpicyPizza(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iSpicyPizzaEquivalent(0) & ~iSpicyPizzaEquivalent(1) & % 5.19/5.42 ~iSpicyPizzaEquivalent(2) & % 5.19/5.42 ~iSpicyPizzaEquivalent(3) & % 5.19/5.42 ~iSpicyPizzaEquivalent(4) & % 5.19/5.42 ~iSpicyPizzaEquivalent(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iSpicyTopping(0) & ~iSpicyTopping(1) & % 5.19/5.42 ~iSpicyTopping(2) & % 5.19/5.42 ~iSpicyTopping(3) & % 5.19/5.42 ~iSpicyTopping(4) & % 5.19/5.42 ~iSpicyTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iSpinachTopping(0) & ~iSpinachTopping(1) & % 5.19/5.42 ~iSpinachTopping(2) & % 5.19/5.42 ~iSpinachTopping(3) & % 5.19/5.42 ~iSpinachTopping(4) & % 5.19/5.42 ~iSpinachTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iSultanaTopping(0) & ~iSultanaTopping(1) & % 5.19/5.42 ~iSultanaTopping(2) & % 5.19/5.42 ~iSultanaTopping(3) & % 5.19/5.42 ~iSultanaTopping(4) & % 5.19/5.42 ~iSultanaTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iSundriedTomatoTopping(0) & % 5.19/5.42 ~iSundriedTomatoTopping(1) & % 5.19/5.42 ~iSundriedTomatoTopping(2) & % 5.19/5.42 ~iSundriedTomatoTopping(3) & % 5.19/5.42 ~iSundriedTomatoTopping(4) & % 5.19/5.42 ~iSundriedTomatoTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iSweetPepperTopping(0) & ~iSweetPepperTopping(1) & % 5.19/5.42 ~iSweetPepperTopping(2) & % 5.19/5.42 ~iSweetPepperTopping(3) & % 5.19/5.42 ~iSweetPepperTopping(4) & % 5.19/5.42 ~iSweetPepperTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iThinAndCrispyBase(0) & ~iThinAndCrispyBase(1) & % 5.19/5.42 ~iThinAndCrispyBase(2) & % 5.19/5.42 ~iThinAndCrispyBase(3) & % 5.19/5.42 ~iThinAndCrispyBase(4) & % 5.19/5.42 ~iThinAndCrispyBase(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iThinAndCrispyPizza(0) & ~iThinAndCrispyPizza(1) & % 5.19/5.42 ~iThinAndCrispyPizza(2) & % 5.19/5.42 ~iThinAndCrispyPizza(3) & % 5.19/5.42 ~iThinAndCrispyPizza(4) & % 5.19/5.42 ~iThinAndCrispyPizza(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iTobascoPepperSauce(0) & ~iTobascoPepperSauce(1) & % 5.19/5.42 ~iTobascoPepperSauce(2) & % 5.19/5.42 ~iTobascoPepperSauce(3) & % 5.19/5.42 ~iTobascoPepperSauce(4) & % 5.19/5.42 ~iTobascoPepperSauce(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iTomatoTopping(0) & ~iTomatoTopping(1) & % 5.19/5.42 ~iTomatoTopping(2) & % 5.19/5.42 ~iTomatoTopping(3) & % 5.19/5.42 ~iTomatoTopping(4) & % 5.19/5.42 ~iTomatoTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iUnclosedPizza(0) & ~iUnclosedPizza(1) & % 5.19/5.42 ~iUnclosedPizza(2) & % 5.19/5.42 ~iUnclosedPizza(3) & % 5.19/5.42 ~iUnclosedPizza(4) & % 5.19/5.42 ~iUnclosedPizza(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iValuePartition(0) & ~iValuePartition(1) & % 5.19/5.42 ~iValuePartition(2) & % 5.19/5.42 ~iValuePartition(3) & % 5.19/5.42 ~iValuePartition(4) & % 5.19/5.42 ~iValuePartition(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iVegetableTopping(0) & ~iVegetableTopping(1) & % 5.19/5.42 ~iVegetableTopping(2) & % 5.19/5.42 ~iVegetableTopping(3) & % 5.19/5.42 ~iVegetableTopping(4) & % 5.19/5.42 ~iVegetableTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iVegetarianPizza(0) & ~iVegetarianPizza(1) & % 5.19/5.42 ~iVegetarianPizza(2) & % 5.19/5.42 ~iVegetarianPizza(3) & % 5.19/5.42 ~iVegetarianPizza(4) & % 5.19/5.42 ~iVegetarianPizza(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iVegetarianPizzaEquivalent1(0) & % 5.19/5.42 ~iVegetarianPizzaEquivalent1(1) & % 5.19/5.42 ~iVegetarianPizzaEquivalent1(2) & % 5.19/5.42 ~iVegetarianPizzaEquivalent1(3) & % 5.19/5.42 ~iVegetarianPizzaEquivalent1(4) & % 5.19/5.42 ~iVegetarianPizzaEquivalent1(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iVegetarianPizzaEquivalent2(0) & % 5.19/5.42 ~iVegetarianPizzaEquivalent2(1) & % 5.19/5.42 ~iVegetarianPizzaEquivalent2(2) & % 5.19/5.42 ~iVegetarianPizzaEquivalent2(3) & % 5.19/5.42 ~iVegetarianPizzaEquivalent2(4) & % 5.19/5.42 ~iVegetarianPizzaEquivalent2(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iVegetarianTopping(0) & ~iVegetarianTopping(1) & % 5.19/5.42 ~iVegetarianTopping(2) & % 5.19/5.42 ~iVegetarianTopping(3) & % 5.19/5.42 ~iVegetarianTopping(4) & % 5.19/5.42 ~iVegetarianTopping(5)). % 5.19/5.42 fof(interp, fi_predicates, ~iVeneziana(0) & ~iVeneziana(1) & ~iVeneziana(2) & % 5.19/5.42 ~iVeneziana(3) & % 5.19/5.42 ~iVeneziana(4) & % 5.19/5.42 ~iVeneziana(5)). % 5.19/5.42 fof(interp, fi_predicates, ~ihasBase(0, 0) & ~ihasBase(0, 1) & ~ihasBase(0, 2) & % 5.19/5.42 ~ihasBase(0, 3) & % 5.19/5.42 ~ihasBase(0, 4) & % 5.19/5.42 ~ihasBase(0, 5) & % 5.19/5.42 ~ihasBase(1, 0) & % 5.19/5.42 ~ihasBase(1, 1) & % 5.19/5.42 ~ihasBase(1, 2) & % 5.19/5.42 ~ihasBase(1, 3) & % 5.19/5.42 ~ihasBase(1, 4) & % 5.19/5.42 ~ihasBase(1, 5) & % 5.19/5.42 ~ihasBase(2, 0) & % 5.19/5.42 ~ihasBase(2, 1) & % 5.19/5.42 ~ihasBase(2, 2) & % 5.19/5.42 ~ihasBase(2, 3) & % 5.19/5.42 ~ihasBase(2, 4) & % 5.19/5.42 ~ihasBase(2, 5) & % 5.19/5.42 ~ihasBase(3, 0) & % 5.19/5.42 ~ihasBase(3, 1) & % 5.19/5.42 ~ihasBase(3, 2) & % 5.19/5.42 ~ihasBase(3, 3) & % 5.19/5.42 ~ihasBase(3, 4) & % 5.19/5.42 ~ihasBase(3, 5) & % 5.19/5.42 ~ihasBase(4, 0) & % 5.19/5.42 ~ihasBase(4, 1) & % 5.19/5.42 ~ihasBase(4, 2) & % 5.19/5.42 ~ihasBase(4, 3) & % 5.19/5.42 ~ihasBase(4, 4) & % 5.19/5.42 ~ihasBase(4, 5) & % 5.19/5.42 ~ihasBase(5, 0) & % 5.19/5.42 ~ihasBase(5, 1) & % 5.19/5.42 ~ihasBase(5, 2) & % 5.19/5.42 ~ihasBase(5, 3) & % 5.19/5.42 ~ihasBase(5, 4) & % 5.19/5.42 ~ihasBase(5, 5)). % 5.19/5.42 fof(interp, fi_predicates, ~ihasCountryOfOrigin(0, 0) & % 5.19/5.42 ~ihasCountryOfOrigin(0, 1) & % 5.19/5.42 ~ihasCountryOfOrigin(0, 2) & % 5.19/5.42 ~ihasCountryOfOrigin(0, 3) & % 5.19/5.42 ~ihasCountryOfOrigin(0, 4) & % 5.19/5.42 ~ihasCountryOfOrigin(0, 5) & % 5.19/5.42 ~ihasCountryOfOrigin(1, 0) & % 5.19/5.42 ~ihasCountryOfOrigin(1, 1) & % 5.19/5.42 ~ihasCountryOfOrigin(1, 2) & % 5.19/5.42 ~ihasCountryOfOrigin(1, 3) & % 5.19/5.42 ~ihasCountryOfOrigin(1, 4) & % 5.19/5.42 ~ihasCountryOfOrigin(1, 5) & % 5.19/5.42 ~ihasCountryOfOrigin(2, 0) & % 5.19/5.42 ~ihasCountryOfOrigin(2, 1) & % 5.19/5.42 ~ihasCountryOfOrigin(2, 2) & % 5.19/5.42 ~ihasCountryOfOrigin(2, 3) & % 5.19/5.42 ~ihasCountryOfOrigin(2, 4) & % 5.19/5.42 ~ihasCountryOfOrigin(2, 5) & % 5.19/5.42 ~ihasCountryOfOrigin(3, 0) & % 5.19/5.42 ~ihasCountryOfOrigin(3, 1) & % 5.19/5.42 ~ihasCountryOfOrigin(3, 2) & % 5.19/5.42 ~ihasCountryOfOrigin(3, 3) & % 5.19/5.42 ~ihasCountryOfOrigin(3, 4) & % 5.19/5.42 ~ihasCountryOfOrigin(3, 5) & % 5.19/5.42 ~ihasCountryOfOrigin(4, 0) & % 5.19/5.42 ~ihasCountryOfOrigin(4, 1) & % 5.19/5.42 ~ihasCountryOfOrigin(4, 2) & % 5.19/5.42 ~ihasCountryOfOrigin(4, 3) & % 5.19/5.42 ~ihasCountryOfOrigin(4, 4) & % 5.19/5.42 ~ihasCountryOfOrigin(4, 5) & % 5.19/5.42 ~ihasCountryOfOrigin(5, 0) & % 5.19/5.42 ~ihasCountryOfOrigin(5, 1) & % 5.19/5.42 ~ihasCountryOfOrigin(5, 2) & % 5.19/5.42 ~ihasCountryOfOrigin(5, 3) & % 5.19/5.42 ~ihasCountryOfOrigin(5, 4) & % 5.19/5.42 ~ihasCountryOfOrigin(5, 5)). % 5.19/5.42 fof(interp, fi_predicates, ~ihasIngredient(0, 0) & ~ihasIngredient(0, 1) & % 5.19/5.42 ~ihasIngredient(0, 2) & % 5.19/5.42 ~ihasIngredient(0, 3) & % 5.19/5.42 ~ihasIngredient(0, 4) & % 5.19/5.42 ~ihasIngredient(0, 5) & % 5.19/5.42 ~ihasIngredient(1, 0) & % 5.19/5.42 ~ihasIngredient(1, 1) & % 5.19/5.42 ~ihasIngredient(1, 2) & % 5.19/5.42 ~ihasIngredient(1, 3) & % 5.19/5.42 ~ihasIngredient(1, 4) & % 5.19/5.42 ~ihasIngredient(1, 5) & % 5.19/5.42 ~ihasIngredient(2, 0) & % 5.19/5.42 ~ihasIngredient(2, 1) & % 5.19/5.42 ~ihasIngredient(2, 2) & % 5.19/5.42 ~ihasIngredient(2, 3) & % 5.19/5.42 ~ihasIngredient(2, 4) & % 5.19/5.42 ~ihasIngredient(2, 5) & % 5.19/5.42 ~ihasIngredient(3, 0) & % 5.19/5.42 ~ihasIngredient(3, 1) & % 5.19/5.42 ~ihasIngredient(3, 2) & % 5.19/5.42 ~ihasIngredient(3, 3) & % 5.19/5.42 ~ihasIngredient(3, 4) & % 5.19/5.42 ~ihasIngredient(3, 5) & % 5.19/5.42 ~ihasIngredient(4, 0) & % 5.19/5.42 ~ihasIngredient(4, 1) & % 5.19/5.42 ~ihasIngredient(4, 2) & % 5.19/5.42 ~ihasIngredient(4, 3) & % 5.19/5.42 ~ihasIngredient(4, 4) & % 5.19/5.42 ~ihasIngredient(4, 5) & % 5.19/5.42 ~ihasIngredient(5, 0) & % 5.19/5.42 ~ihasIngredient(5, 1) & % 5.19/5.42 ~ihasIngredient(5, 2) & % 5.19/5.42 ~ihasIngredient(5, 3) & % 5.19/5.42 ~ihasIngredient(5, 4) & % 5.19/5.42 ~ihasIngredient(5, 5)). % 5.19/5.42 fof(interp, fi_predicates, ~ihasSpiciness(0, 0) & ~ihasSpiciness(0, 1) & % 5.19/5.42 ~ihasSpiciness(0, 2) & % 5.19/5.42 ~ihasSpiciness(0, 3) & % 5.19/5.42 ~ihasSpiciness(0, 4) & % 5.19/5.42 ~ihasSpiciness(0, 5) & % 5.19/5.42 ~ihasSpiciness(1, 0) & % 5.19/5.42 ~ihasSpiciness(1, 1) & % 5.19/5.42 ~ihasSpiciness(1, 2) & % 5.19/5.42 ~ihasSpiciness(1, 3) & % 5.19/5.42 ~ihasSpiciness(1, 4) & % 5.19/5.42 ~ihasSpiciness(1, 5) & % 5.19/5.42 ~ihasSpiciness(2, 0) & % 5.19/5.42 ~ihasSpiciness(2, 1) & % 5.19/5.42 ~ihasSpiciness(2, 2) & % 5.19/5.42 ~ihasSpiciness(2, 3) & % 5.19/5.42 ~ihasSpiciness(2, 4) & % 5.19/5.42 ~ihasSpiciness(2, 5) & % 5.19/5.42 ~ihasSpiciness(3, 0) & % 5.19/5.42 ~ihasSpiciness(3, 1) & % 5.19/5.42 ~ihasSpiciness(3, 2) & % 5.19/5.42 ~ihasSpiciness(3, 3) & % 5.19/5.42 ~ihasSpiciness(3, 4) & % 5.19/5.42 ~ihasSpiciness(3, 5) & % 5.19/5.42 ~ihasSpiciness(4, 0) & % 5.19/5.42 ~ihasSpiciness(4, 1) & % 5.19/5.42 ~ihasSpiciness(4, 2) & % 5.19/5.42 ~ihasSpiciness(4, 3) & % 5.19/5.42 ~ihasSpiciness(4, 4) & % 5.19/5.42 ~ihasSpiciness(4, 5) & % 5.19/5.42 ~ihasSpiciness(5, 0) & % 5.19/5.42 ~ihasSpiciness(5, 1) & % 5.19/5.42 ~ihasSpiciness(5, 2) & % 5.19/5.42 ~ihasSpiciness(5, 3) & % 5.19/5.42 ~ihasSpiciness(5, 4) & % 5.19/5.42 ~ihasSpiciness(5, 5)). % 5.19/5.42 fof(interp, fi_predicates, ~ihasTopping(0, 0) & ~ihasTopping(0, 1) & % 5.19/5.42 ~ihasTopping(0, 2) & % 5.19/5.42 ~ihasTopping(0, 3) & % 5.19/5.42 ~ihasTopping(0, 4) & % 5.19/5.42 ~ihasTopping(0, 5) & % 5.19/5.42 ~ihasTopping(1, 0) & % 5.19/5.42 ~ihasTopping(1, 1) & % 5.19/5.42 ~ihasTopping(1, 2) & % 5.19/5.42 ~ihasTopping(1, 3) & % 5.19/5.42 ~ihasTopping(1, 4) & % 5.19/5.42 ~ihasTopping(1, 5) & % 5.19/5.42 ~ihasTopping(2, 0) & % 5.19/5.42 ~ihasTopping(2, 1) & % 5.19/5.42 ~ihasTopping(2, 2) & % 5.19/5.42 ~ihasTopping(2, 3) & % 5.19/5.42 ~ihasTopping(2, 4) & % 5.19/5.42 ~ihasTopping(2, 5) & % 5.19/5.42 ~ihasTopping(3, 0) & % 5.19/5.42 ~ihasTopping(3, 1) & % 5.19/5.42 ~ihasTopping(3, 2) & % 5.19/5.42 ~ihasTopping(3, 3) & % 5.19/5.42 ~ihasTopping(3, 4) & % 5.19/5.42 ~ihasTopping(3, 5) & % 5.19/5.42 ~ihasTopping(4, 0) & % 5.19/5.42 ~ihasTopping(4, 1) & % 5.19/5.42 ~ihasTopping(4, 2) & % 5.19/5.42 ~ihasTopping(4, 3) & % 5.19/5.42 ~ihasTopping(4, 4) & % 5.19/5.42 ~ihasTopping(4, 5) & % 5.19/5.42 ~ihasTopping(5, 0) & % 5.19/5.42 ~ihasTopping(5, 1) & % 5.19/5.42 ~ihasTopping(5, 2) & % 5.19/5.42 ~ihasTopping(5, 3) & % 5.19/5.42 ~ihasTopping(5, 4) & % 5.19/5.42 ~ihasTopping(5, 5)). % 5.19/5.42 fof(interp, fi_predicates, ~iisBaseOf(0, 0) & ~iisBaseOf(0, 1) & % 5.19/5.42 ~iisBaseOf(0, 2) & % 5.19/5.42 ~iisBaseOf(0, 3) & % 5.19/5.42 ~iisBaseOf(0, 4) & % 5.19/5.42 ~iisBaseOf(0, 5) & % 5.19/5.42 ~iisBaseOf(1, 0) & % 5.19/5.42 ~iisBaseOf(1, 1) & % 5.19/5.42 ~iisBaseOf(1, 2) & % 5.19/5.42 ~iisBaseOf(1, 3) & % 5.19/5.42 ~iisBaseOf(1, 4) & % 5.19/5.42 ~iisBaseOf(1, 5) & % 5.19/5.42 ~iisBaseOf(2, 0) & % 5.19/5.42 ~iisBaseOf(2, 1) & % 5.19/5.42 ~iisBaseOf(2, 2) & % 5.19/5.42 ~iisBaseOf(2, 3) & % 5.19/5.42 ~iisBaseOf(2, 4) & % 5.19/5.42 ~iisBaseOf(2, 5) & % 5.19/5.42 ~iisBaseOf(3, 0) & % 5.19/5.42 ~iisBaseOf(3, 1) & % 5.19/5.42 ~iisBaseOf(3, 2) & % 5.19/5.42 ~iisBaseOf(3, 3) & % 5.19/5.42 ~iisBaseOf(3, 4) & % 5.19/5.42 ~iisBaseOf(3, 5) & % 5.19/5.42 ~iisBaseOf(4, 0) & % 5.19/5.42 ~iisBaseOf(4, 1) & % 5.19/5.42 ~iisBaseOf(4, 2) & % 5.19/5.42 ~iisBaseOf(4, 3) & % 5.19/5.42 ~iisBaseOf(4, 4) & % 5.19/5.42 ~iisBaseOf(4, 5) & % 5.19/5.42 ~iisBaseOf(5, 0) & % 5.19/5.42 ~iisBaseOf(5, 1) & % 5.19/5.42 ~iisBaseOf(5, 2) & % 5.19/5.42 ~iisBaseOf(5, 3) & % 5.19/5.42 ~iisBaseOf(5, 4) & % 5.19/5.42 ~iisBaseOf(5, 5)). % 5.19/5.42 fof(interp, fi_predicates, ~iisIngredientOf(0, 0) & ~iisIngredientOf(0, 1) & % 5.19/5.42 ~iisIngredientOf(0, 2) & % 5.19/5.42 ~iisIngredientOf(0, 3) & % 5.19/5.42 ~iisIngredientOf(0, 4) & % 5.19/5.42 ~iisIngredientOf(0, 5) & % 5.19/5.42 ~iisIngredientOf(1, 0) & % 5.19/5.42 ~iisIngredientOf(1, 1) & % 5.19/5.42 ~iisIngredientOf(1, 2) & % 5.19/5.42 ~iisIngredientOf(1, 3) & % 5.19/5.42 ~iisIngredientOf(1, 4) & % 5.19/5.42 ~iisIngredientOf(1, 5) & % 5.19/5.42 ~iisIngredientOf(2, 0) & % 5.19/5.42 ~iisIngredientOf(2, 1) & % 5.19/5.42 ~iisIngredientOf(2, 2) & % 5.19/5.42 ~iisIngredientOf(2, 3) & % 5.19/5.42 ~iisIngredientOf(2, 4) & % 5.19/5.42 ~iisIngredientOf(2, 5) & % 5.19/5.42 ~iisIngredientOf(3, 0) & % 5.19/5.42 ~iisIngredientOf(3, 1) & % 5.19/5.42 ~iisIngredientOf(3, 2) & % 5.19/5.42 ~iisIngredientOf(3, 3) & % 5.19/5.42 ~iisIngredientOf(3, 4) & % 5.19/5.42 ~iisIngredientOf(3, 5) & % 5.19/5.42 ~iisIngredientOf(4, 0) & % 5.19/5.42 ~iisIngredientOf(4, 1) & % 5.19/5.42 ~iisIngredientOf(4, 2) & % 5.19/5.42 ~iisIngredientOf(4, 3) & % 5.19/5.42 ~iisIngredientOf(4, 4) & % 5.19/5.42 ~iisIngredientOf(4, 5) & % 5.19/5.42 ~iisIngredientOf(5, 0) & % 5.19/5.42 ~iisIngredientOf(5, 1) & % 5.19/5.42 ~iisIngredientOf(5, 2) & % 5.19/5.42 ~iisIngredientOf(5, 3) & % 5.19/5.42 ~iisIngredientOf(5, 4) & % 5.19/5.42 ~iisIngredientOf(5, 5)). % 5.19/5.42 fof(interp, fi_predicates, ~iisToppingOf(0, 0) & ~iisToppingOf(0, 1) & % 5.19/5.42 ~iisToppingOf(0, 2) & % 5.19/5.42 ~iisToppingOf(0, 3) & % 5.19/5.42 ~iisToppingOf(0, 4) & % 5.19/5.42 ~iisToppingOf(0, 5) & % 5.19/5.42 ~iisToppingOf(1, 0) & % 5.19/5.42 ~iisToppingOf(1, 1) & % 5.19/5.42 ~iisToppingOf(1, 2) & % 5.19/5.42 ~iisToppingOf(1, 3) & % 5.19/5.42 ~iisToppingOf(1, 4) & % 5.19/5.42 ~iisToppingOf(1, 5) & % 5.19/5.42 ~iisToppingOf(2, 0) & % 5.19/5.42 ~iisToppingOf(2, 1) & % 5.19/5.42 ~iisToppingOf(2, 2) & % 5.19/5.42 ~iisToppingOf(2, 3) & % 5.19/5.42 ~iisToppingOf(2, 4) & % 5.19/5.42 ~iisToppingOf(2, 5) & % 5.19/5.42 ~iisToppingOf(3, 0) & % 5.19/5.42 ~iisToppingOf(3, 1) & % 5.19/5.42 ~iisToppingOf(3, 2) & % 5.19/5.42 ~iisToppingOf(3, 3) & % 5.19/5.42 ~iisToppingOf(3, 4) & % 5.19/5.42 ~iisToppingOf(3, 5) & % 5.19/5.42 ~iisToppingOf(4, 0) & % 5.19/5.42 ~iisToppingOf(4, 1) & % 5.19/5.42 ~iisToppingOf(4, 2) & % 5.19/5.42 ~iisToppingOf(4, 3) & % 5.19/5.42 ~iisToppingOf(4, 4) & % 5.19/5.42 ~iisToppingOf(4, 5) & % 5.19/5.42 ~iisToppingOf(5, 0) & % 5.19/5.42 ~iisToppingOf(5, 1) & % 5.19/5.42 ~iisToppingOf(5, 2) & % 5.19/5.42 ~iisToppingOf(5, 3) & % 5.19/5.42 ~iisToppingOf(5, 4) & % 5.19/5.42 ~iisToppingOf(5, 5)). % 5.19/5.42 fof(interp, fi_predicates, ~iowlNothing(0) & ~iowlNothing(1) & ~iowlNothing(2) & % 5.19/5.42 ~iowlNothing(3) & % 5.19/5.42 ~iowlNothing(4) & % 5.19/5.42 ~iowlNothing(5)). % 5.19/5.42 fof(interp, fi_predicates, iowlThing(0) & ~iowlThing(1) & iowlThing(2) & % 5.19/5.42 iowlThing(3) & % 5.19/5.42 iowlThing(4) & % 5.19/5.42 iowlThing(5)). % 5.19/5.42 fof(interp, fi_predicates, ~xsd_integer(0) & ~xsd_integer(1) & ~xsd_integer(2) & % 5.19/5.42 ~xsd_integer(3) & % 5.19/5.42 ~xsd_integer(4) & % 5.19/5.42 ~xsd_integer(5)). % 5.19/5.42 fof(interp, fi_predicates, ~xsd_string(0) & ~xsd_string(1) & ~xsd_string(2) & % 5.19/5.42 ~xsd_string(3) & % 5.19/5.42 ~xsd_string(4) & % 5.19/5.42 ~xsd_string(5)). % 5.19/5.42 % SZS output end FiniteModel for theBenchmark.p % 5.19/5.42 % 6 lemma(s) from E % 5.19/5.42 % cnf(cl, axiom, abstractDomain(iEngland)). % 5.19/5.42 % cnf(cl, axiom, abstractDomain(iGermany)). % 5.19/5.42 % cnf(cl, axiom, abstractDomain(iItaly)). % 5.19/5.42 % cnf(cl, axiom, abstractDomain(iFrance)). % 5.19/5.42 % cnf(cl, axiom, abstractDomain(iAmerica)). % 5.19/5.42 % cnf(cl, axiom, ~abstractDomain(esk2_0)). % 5.19/5.42 % 113 pred(s) % 5.19/5.42 % 168 func(s) % 5.19/5.42 % 1 sort(s) % 5.19/5.42 % 1103 clause(s) % 5.19/5.42 % Instantiating 1 (5065 ms) % 5.19/5.42 % Solving (5066 ms) % 5.19/5.42 % Instantiating 2 (5066 ms) % 5.19/5.42 % Solving (5067 ms) % 5.19/5.42 % Instantiating 3 (5068 ms) % 5.19/5.42 % Solving (5070 ms) % 5.19/5.42 % Instantiating 4 (5070 ms) % 5.19/5.42 % Solving (5073 ms) % 5.19/5.42 % Instantiating 5 (5073 ms) % 5.19/5.42 % Solving (5078 ms) % 5.19/5.42 % Instantiating 6 (5078 ms) % 5.19/5.42 % Solving (5084 ms) % 5.19/5.42 % % 5.19/5.42 % 1 model found (5089 ms) %------------------------------------------------------------------------------