%------------------------------------------------------------------------------ % File : Crossbow---0.1 % Problem : LCL665+1.020 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : do_Crossbow---0.1 %s % Computer : n004.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 : Mon Sep 7 11:17:49 AM UTC 2026 % Result : CounterSatisfiable 6.64s 6.93s % Output : FiniteModel 6.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL665+1.020 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : do_Crossbow---0.1 %s % 0.09/0.34 % Computer : n004.cluster.edu % 0.09/0.34 % Model : x86_64 x86_64 % 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.34 % Memory : 8046.5625MB % 0.09/0.34 % OS : Linux 6.8.0-71-generic % 0.09/0.34 % CPULimit : 300 % 0.09/0.34 % WCLimit : 300 % 0.09/0.34 % DateTime : Fri Sep 4 17:10:44 UTC 2026 % 0.09/0.34 % CPUTime : % 0.09/0.34 /export/starexec/sandbox/solver/bin % 0.09/0.35 crossbow.opt % 0.09/0.35 do_Crossbow---0.1 % 0.09/0.35 eprover % 0.09/0.35 runsolver % 0.09/0.35 starexec_run_Crossbow---0.1 % 6.64/6.93 % SZS status CounterSatisfiable for theBenchmark.p % 6.64/6.93 % SZS output start FiniteModel for theBenchmark.p % 6.64/6.93 % domain size: 1 % 6.64/6.93 fof(interp, fi_domain, ![X] : X = 0). % 6.64/6.93 fof(interp, fi_functors, esk100_15(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk101_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk102_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk103_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk104_15(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk105_15(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk106_15(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk107_13(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk108_13(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk109_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk10_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk110_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk111_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk112_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk113_13(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk114_13(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk115_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk116_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk117_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk118_13(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk119_13(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk11_19(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk120_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk121_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk122_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk123_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk124_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk125_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk126_13(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk127_13(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk128_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk129_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk12_19(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk130_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk131_13(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk132_13(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk133_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk134_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk135_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk136_13(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk137_13(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk138_13(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk139_11(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk13_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk140_11(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk141_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk142_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk143_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk144_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk145_11(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk146_11(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk147_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk148_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk149_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk14_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk150_11(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk151_11(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk152_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk153_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk154_12(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk155_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk156_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk157_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk158_11(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk159_11(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk15_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk160_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk161_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk162_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk163_11(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk164_11(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk165_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk166_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk167_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk168_11(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk169_11(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk16_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk170_11(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk171_9(0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk172_9(0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk173_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk174_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk175_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk176_9(0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk177_9(0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk178_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk179_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk17_19(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk180_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk181_9(0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk182_9(0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk183_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk184_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk185_10(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk186_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk187_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk188_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk189_9(0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk18_19(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk190_9(0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk191_9(0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk192_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk193_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk194_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk195_9(0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk196_9(0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk197_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk198_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk199_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk19_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk1_0 = 0). % 6.64/6.93 fof(interp, fi_functors, esk200_9(0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk201_9(0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk202_7(0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk203_7(0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk204_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk205_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk206_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk207_7(0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk208_7(0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk209_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk20_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk210_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk211_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk212_7(0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk213_7(0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk214_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk215_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk216_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk217_8(0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk218_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk219_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk21_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk220_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk221_7(0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk222_7(0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk223_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk224_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk225_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk226_7(0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk227_7(0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk228_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk229_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk22_19(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk230_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk231_7(0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk232_7(0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk233_7(0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk234_5(0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk235_5(0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk236_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk237_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk238_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk239_5(0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk23_19(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk240_5(0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk241_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk242_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk243_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk244_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk245_5(0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk246_5(0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk247_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk248_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk249_6(0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk24_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk250_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk251_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk252_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk253_5(0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk254_5(0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk255_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk256_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk257_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk258_5(0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk259_5(0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk25_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk260_5(0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk261_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk262_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk263_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk264_5(0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk265_5(0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk266_3(0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk267_3(0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk268_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk269_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk26_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk270_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk271_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk272_3(0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk273_3(0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk274_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk275_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk276_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk277_3(0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk278_3(0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk279_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk27_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk280_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk281_4(0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk282_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk283_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk284_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk285_3(0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk286_3(0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk287_3(0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk288_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk289_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk28_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk290_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk291_3(0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk292_3(0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk293_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk294_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk295_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk296_3(0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk297_3(0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk298_1(0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk299_1(0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk29_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk2_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk300_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk301_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk302_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk303_1(0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk304_1(0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk305_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk306_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk307_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk308_1(0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk309_1(0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk30_19(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk310_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk311_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk312_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk313_2(0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk314_1(0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk315_1(0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk316_1(0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk317_1(0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk318_1(0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk319_1(0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk31_19(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk320_1(0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk321_0 = 0). % 6.64/6.93 fof(interp, fi_functors, esk322_0 = 0). % 6.64/6.93 fof(interp, fi_functors, esk323_0 = 0). % 6.64/6.93 fof(interp, fi_functors, esk324_0 = 0). % 6.64/6.93 fof(interp, fi_functors, esk32_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk33_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk34_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk35_19(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk36_19(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk37_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk38_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk39_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk3_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk40_19(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk41_19(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk42_19(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk43_17(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk44_17(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk45_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk46_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk47_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk48_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk49_17(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk4_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk50_17(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk51_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk52_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk53_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk54_17(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk55_17(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk56_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk57_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk58_18(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk59_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk5_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk60_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk61_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk62_17(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk63_17(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk64_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk65_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk66_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk67_17(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk68_17(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk69_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk6_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk70_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk71_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk72_17(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk73_17(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk74_17(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk75_15(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk76_15(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk77_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk78_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk79_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk7_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk80_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk81_15(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk82_15(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk83_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk84_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk85_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk86_15(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk87_15(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk88_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk89_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk8_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk90_16(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk91_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk92_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk93_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk94_15(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk95_15(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk96_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk97_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk98_14(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk99_15(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_functors, esk9_20(0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0) = 0). % 6.64/6.93 fof(interp, fi_predicates, ~p101(0)). % 6.64/6.93 fof(interp, fi_predicates, p102(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p103(0)). % 6.64/6.93 fof(interp, fi_predicates, p104(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p105(0)). % 6.64/6.93 fof(interp, fi_predicates, p106(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p11(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p111(0)). % 6.64/6.93 fof(interp, fi_predicates, p112(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p113(0)). % 6.64/6.93 fof(interp, fi_predicates, p114(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p115(0)). % 6.64/6.93 fof(interp, fi_predicates, p116(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p12(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p121(0)). % 6.64/6.93 fof(interp, fi_predicates, p122(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p123(0)). % 6.64/6.93 fof(interp, fi_predicates, p124(0)). % 6.64/6.93 fof(interp, fi_predicates, p125(0)). % 6.64/6.93 fof(interp, fi_predicates, p126(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p13(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p131(0)). % 6.64/6.93 fof(interp, fi_predicates, p132(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p133(0)). % 6.64/6.93 fof(interp, fi_predicates, p134(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p135(0)). % 6.64/6.93 fof(interp, fi_predicates, p136(0)). % 6.64/6.93 fof(interp, fi_predicates, p14(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p141(0)). % 6.64/6.93 fof(interp, fi_predicates, p142(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p143(0)). % 6.64/6.93 fof(interp, fi_predicates, p144(0)). % 6.64/6.93 fof(interp, fi_predicates, p145(0)). % 6.64/6.93 fof(interp, fi_predicates, p146(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p15(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p151(0)). % 6.64/6.93 fof(interp, fi_predicates, p152(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p153(0)). % 6.64/6.93 fof(interp, fi_predicates, p154(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p155(0)). % 6.64/6.93 fof(interp, fi_predicates, p156(0)). % 6.64/6.93 fof(interp, fi_predicates, p16(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p161(0)). % 6.64/6.93 fof(interp, fi_predicates, p162(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p163(0)). % 6.64/6.93 fof(interp, fi_predicates, p164(0)). % 6.64/6.93 fof(interp, fi_predicates, p165(0)). % 6.64/6.93 fof(interp, fi_predicates, p166(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p171(0)). % 6.64/6.93 fof(interp, fi_predicates, p172(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p173(0)). % 6.64/6.93 fof(interp, fi_predicates, p174(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p175(0)). % 6.64/6.93 fof(interp, fi_predicates, p176(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p181(0)). % 6.64/6.93 fof(interp, fi_predicates, p182(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p183(0)). % 6.64/6.93 fof(interp, fi_predicates, p184(0)). % 6.64/6.93 fof(interp, fi_predicates, p185(0)). % 6.64/6.93 fof(interp, fi_predicates, p186(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p191(0)). % 6.64/6.93 fof(interp, fi_predicates, p192(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p193(0)). % 6.64/6.93 fof(interp, fi_predicates, p194(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p195(0)). % 6.64/6.93 fof(interp, fi_predicates, p196(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p201(0)). % 6.64/6.93 fof(interp, fi_predicates, p202(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p203(0)). % 6.64/6.93 fof(interp, fi_predicates, p204(0)). % 6.64/6.93 fof(interp, fi_predicates, p205(0)). % 6.64/6.93 fof(interp, fi_predicates, p206(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p21(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p211(0)). % 6.64/6.93 fof(interp, fi_predicates, p212(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p213(0)). % 6.64/6.93 fof(interp, fi_predicates, p214(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p215(0)). % 6.64/6.93 fof(interp, fi_predicates, p216(0)). % 6.64/6.93 fof(interp, fi_predicates, p22(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p23(0)). % 6.64/6.93 fof(interp, fi_predicates, p24(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p25(0)). % 6.64/6.93 fof(interp, fi_predicates, p26(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p31(0)). % 6.64/6.93 fof(interp, fi_predicates, p32(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p33(0)). % 6.64/6.93 fof(interp, fi_predicates, p34(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p35(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p36(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p41(0)). % 6.64/6.93 fof(interp, fi_predicates, p42(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p43(0)). % 6.64/6.93 fof(interp, fi_predicates, p44(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p45(0)). % 6.64/6.93 fof(interp, fi_predicates, p46(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p51(0)). % 6.64/6.93 fof(interp, fi_predicates, p52(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p53(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p54(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p55(0)). % 6.64/6.93 fof(interp, fi_predicates, p56(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p61(0)). % 6.64/6.93 fof(interp, fi_predicates, p62(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p63(0)). % 6.64/6.93 fof(interp, fi_predicates, p64(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p65(0)). % 6.64/6.93 fof(interp, fi_predicates, p66(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p71(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p72(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p73(0)). % 6.64/6.93 fof(interp, fi_predicates, p74(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p75(0)). % 6.64/6.93 fof(interp, fi_predicates, p76(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p81(0)). % 6.64/6.93 fof(interp, fi_predicates, p82(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p83(0)). % 6.64/6.93 fof(interp, fi_predicates, p84(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p85(0)). % 6.64/6.93 fof(interp, fi_predicates, p86(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p91(0)). % 6.64/6.93 fof(interp, fi_predicates, p92(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p93(0)). % 6.64/6.93 fof(interp, fi_predicates, p94(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p95(0)). % 6.64/6.93 fof(interp, fi_predicates, ~p96(0)). % 6.64/6.93 fof(interp, fi_predicates, r1(0, 0)). % 6.64/6.93 % SZS output end FiniteModel for theBenchmark.p % 6.64/6.93 % 0 lemma(s) from E % 6.64/6.93 % 815 pred(s) % 6.64/6.93 % 324 func(s) % 6.64/6.93 % 1 sort(s) % 6.64/6.93 % 1339 clause(s) % 6.64/6.93 % Instantiating 1 (6238 ms) % 6.64/6.93 % Solving (6243 ms) % 6.64/6.93 % % 6.64/6.93 % 1 model found (6250 ms) %------------------------------------------------------------------------------