CSE_E---1.7.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : CSE_E---1.7
% Problem  : PLA031-1.007 : TPTP v9.2.1. Released v3.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d

% Computer : n010.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue May  5 05:01:26 PM UTC 2026

% Result   : Unsatisfiable 242.22s 127.67s
% Output   : CNFRefutation 253.22s
% Verified : 
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_4177)

% Comments : 
%------------------------------------------------------------------------------
cnf(board5,axiom,
    ( s(X1,X2,X3,X4,X5,X6,truck3,X8,X9,X10,X11,X7)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X7)
    | ~ neq(X8,truck3)
    | ~ neq(X9,truck3) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board5) ).

cnf(board3,axiom,
    ( s(X1,X2,X3,X4,X5,X6,truck2,X8,X9,X10,X7,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X7,X11)
    | ~ neq(X8,truck2)
    | ~ neq(X9,truck2) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board3) ).

cnf(board1,axiom,
    ( s(X1,X2,X3,X4,X5,X6,truck1,X8,X9,X7,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X7,X10,X11)
    | ~ neq(X8,truck1)
    | ~ neq(X9,truck1) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board1) ).

cnf(board11,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,truck3,X9,X10,X11,X8)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X8)
    | ~ neq(X7,truck3)
    | ~ neq(X9,truck3) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board11) ).

cnf(board9,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,truck2,X9,X10,X8,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X8,X11)
    | ~ neq(X7,truck2)
    | ~ neq(X9,truck2) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board9) ).

cnf(board7,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,truck1,X9,X8,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X8,X10,X11)
    | ~ neq(X7,truck1)
    | ~ neq(X9,truck1) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board7) ).

cnf(board17,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,truck3,X10,X11,X9)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X9)
    | ~ neq(X7,truck3)
    | ~ neq(X8,truck3) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board17) ).

cnf(board15,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,truck2,X10,X9,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X9,X11)
    | ~ neq(X7,truck2)
    | ~ neq(X8,truck2) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board15) ).

cnf(board13,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,truck1,X9,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X9,X10,X11)
    | ~ neq(X7,truck1)
    | ~ neq(X8,truck1) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board13) ).

cnf(drive3,axiom,
    ( s(X1,X2,X3,X4,X5,X6,truck3,X7,X8,X9,X10,X12)
    | ~ s(X1,X2,X3,X4,X5,X6,truck3,X7,X8,X9,X10,X11)
    | ~ link(X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',drive3) ).

cnf(drive2,axiom,
    ( s(X1,X2,X3,X4,X5,X6,truck2,X7,X8,X9,X12,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,truck2,X7,X8,X9,X10,X11)
    | ~ link(X10,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',drive2) ).

cnf(drive1,axiom,
    ( s(X1,X2,X3,X4,X5,X6,truck1,X7,X8,X12,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,truck1,X7,X8,X9,X10,X11)
    | ~ link(X9,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',drive1) ).

cnf(drive6,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,truck3,X8,X9,X10,X12)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,truck3,X8,X9,X10,X11)
    | ~ link(X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',drive6) ).

cnf(drive5,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,truck2,X8,X9,X12,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,truck2,X8,X9,X10,X11)
    | ~ link(X10,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',drive5) ).

cnf(drive4,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,truck1,X8,X12,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,truck1,X8,X9,X10,X11)
    | ~ link(X9,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',drive4) ).

cnf(drive9,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,truck3,X9,X10,X12)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,truck3,X9,X10,X11)
    | ~ link(X11,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',drive9) ).

cnf(drive8,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,truck2,X9,X12,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,truck2,X9,X10,X11)
    | ~ link(X10,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',drive8) ).

cnf(drive7,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,truck1,X12,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,truck1,X9,X10,X11)
    | ~ link(X9,X12) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',drive7) ).

cnf(walk3,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X13,X10,X11,X12)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
    | ~ path(X9,X13) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',walk3) ).

cnf(walk2,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X13,X9,X10,X11,X12)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
    | ~ path(X8,X13) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',walk2) ).

cnf(walk1,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X13,X8,X9,X10,X11,X12)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
    | ~ path(X7,X13) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',walk1) ).

cnf(load5,axiom,
    ( s(truck3,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load5) ).

cnf(load3,axiom,
    ( s(truck2,X2,X3,X4,X5,X6,X7,X8,X9,X10,X1,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X1,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load3) ).

cnf(load1,axiom,
    ( s(truck1,X2,X3,X4,X5,X6,X7,X8,X9,X1,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X1,X10,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load1) ).

cnf(load11,axiom,
    ( s(X1,truck3,X3,X4,X5,X6,X7,X8,X9,X10,X11,X2)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X2) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load11) ).

cnf(load9,axiom,
    ( s(X1,truck2,X3,X4,X5,X6,X7,X8,X9,X10,X2,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X2,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load9) ).

cnf(load7,axiom,
    ( s(X1,truck1,X3,X4,X5,X6,X7,X8,X9,X2,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X2,X10,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load7) ).

cnf(load17,axiom,
    ( s(X1,X2,truck3,X4,X5,X6,X7,X8,X9,X10,X11,X3)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X3) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load17) ).

cnf(load15,axiom,
    ( s(X1,X2,truck2,X4,X5,X6,X7,X8,X9,X10,X3,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X3,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load15) ).

cnf(load13,axiom,
    ( s(X1,X2,truck1,X4,X5,X6,X7,X8,X9,X3,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X3,X10,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load13) ).

cnf(load23,axiom,
    ( s(X1,X2,X3,truck3,X5,X6,X7,X8,X9,X10,X11,X4)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X4) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load23) ).

cnf(load21,axiom,
    ( s(X1,X2,X3,truck2,X5,X6,X7,X8,X9,X10,X4,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X4,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load21) ).

cnf(load19,axiom,
    ( s(X1,X2,X3,truck1,X5,X6,X7,X8,X9,X4,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X4,X10,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load19) ).

cnf(load29,axiom,
    ( s(X1,X2,X3,X4,truck3,X6,X7,X8,X9,X10,X11,X5)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X5) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load29) ).

cnf(load27,axiom,
    ( s(X1,X2,X3,X4,truck2,X6,X7,X8,X9,X10,X5,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X5,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load27) ).

cnf(load25,axiom,
    ( s(X1,X2,X3,X4,truck1,X6,X7,X8,X9,X5,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X5,X10,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load25) ).

cnf(load35,axiom,
    ( s(X1,X2,X3,X4,X5,truck3,X7,X8,X9,X10,X11,X6)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X6) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load35) ).

cnf(load33,axiom,
    ( s(X1,X2,X3,X4,X5,truck2,X7,X8,X9,X10,X6,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X6,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load33) ).

cnf(load31,axiom,
    ( s(X1,X2,X3,X4,X5,truck1,X7,X8,X9,X6,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X6,X10,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load31) ).

cnf(load2,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X1,X10,X11)
    | ~ s(truck1,X2,X3,X4,X5,X6,X7,X8,X9,X1,X10,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load2) ).

cnf(load4,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X1,X11)
    | ~ s(truck2,X2,X3,X4,X5,X6,X7,X8,X9,X10,X1,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load4) ).

cnf(load6,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1)
    | ~ s(truck3,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load6) ).

cnf(load8,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X2,X10,X11)
    | ~ s(X1,truck1,X3,X4,X5,X6,X7,X8,X9,X2,X10,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load8) ).

cnf(load10,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X2,X11)
    | ~ s(X1,truck2,X3,X4,X5,X6,X7,X8,X9,X10,X2,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load10) ).

cnf(load12,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X2)
    | ~ s(X1,truck3,X3,X4,X5,X6,X7,X8,X9,X10,X11,X2) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load12) ).

cnf(load14,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X3,X10,X11)
    | ~ s(X1,X2,truck1,X4,X5,X6,X7,X8,X9,X3,X10,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load14) ).

cnf(load16,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X3,X11)
    | ~ s(X1,X2,truck2,X4,X5,X6,X7,X8,X9,X10,X3,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load16) ).

cnf(load18,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X3)
    | ~ s(X1,X2,truck3,X4,X5,X6,X7,X8,X9,X10,X11,X3) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load18) ).

cnf(load20,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X4,X10,X11)
    | ~ s(X1,X2,X3,truck1,X5,X6,X7,X8,X9,X4,X10,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load20) ).

cnf(load22,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X4,X11)
    | ~ s(X1,X2,X3,truck2,X5,X6,X7,X8,X9,X10,X4,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load22) ).

cnf(load24,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X4)
    | ~ s(X1,X2,X3,truck3,X5,X6,X7,X8,X9,X10,X11,X4) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load24) ).

cnf(load26,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X5,X10,X11)
    | ~ s(X1,X2,X3,X4,truck1,X6,X7,X8,X9,X5,X10,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load26) ).

cnf(load28,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X5,X11)
    | ~ s(X1,X2,X3,X4,truck2,X6,X7,X8,X9,X10,X5,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load28) ).

cnf(load30,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X5)
    | ~ s(X1,X2,X3,X4,truck3,X6,X7,X8,X9,X10,X11,X5) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load30) ).

cnf(load32,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X6,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,truck1,X7,X8,X9,X6,X10,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load32) ).

cnf(load34,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X6,X11)
    | ~ s(X1,X2,X3,X4,X5,truck2,X7,X8,X9,X10,X6,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load34) ).

cnf(load36,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X6)
    | ~ s(X1,X2,X3,X4,X5,truck3,X7,X8,X9,X10,X11,X6) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',load36) ).

cnf(board2,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X7,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,truck1,X8,X9,X7,X10,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board2) ).

cnf(board4,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X7,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,truck2,X8,X9,X10,X7,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board4) ).

cnf(board6,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X7)
    | ~ s(X1,X2,X3,X4,X5,X6,truck3,X8,X9,X10,X11,X7) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board6) ).

cnf(board8,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X8,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,truck1,X9,X8,X10,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board8) ).

cnf(board10,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X8,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,truck2,X9,X10,X8,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board10) ).

cnf(board12,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X8)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,truck3,X9,X10,X11,X8) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board12) ).

cnf(board14,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X9,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,truck1,X9,X10,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board14) ).

cnf(board16,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X9,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,truck2,X10,X9,X11) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board16) ).

cnf(board18,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X9)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,truck3,X10,X11,X9) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',board18) ).

cnf(goal,negated_conjecture,
    ~ s(s0,s1,s1,s1,s2,s2,s0,s2,X1,s1,s0,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).

cnf(init,axiom,
    s(s2,s0,s1,s1,s2,s1,s0,s0,s1,s1,s0,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',init) ).

cnf(neq100,axiom,
    ~ neq(p2_1,p2_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq100) ).

cnf(neq89,axiom,
    ~ neq(p2_0,p2_0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq89) ).

cnf(neq78,axiom,
    ~ neq(p1_2,p1_2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq78) ).

cnf(neq67,axiom,
    ~ neq(p0_1,p0_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq67) ).

cnf(neq56,axiom,
    ~ neq(s2,s2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq56) ).

cnf(neq45,axiom,
    ~ neq(s1,s1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq45) ).

cnf(neq34,axiom,
    ~ neq(s0,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq34) ).

cnf(neq23,axiom,
    ~ neq(truck3,truck3),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq23) ).

cnf(neq12,axiom,
    ~ neq(truck2,truck2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq12) ).

cnf(neq1,axiom,
    ~ neq(truck1,truck1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq1) ).

cnf(map10,axiom,
    path(p2_0,s2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map10) ).

cnf(map12,axiom,
    path(p2_0,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map12) ).

cnf(map8,axiom,
    path(p1_2,s2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map8) ).

cnf(map6,axiom,
    path(p1_2,s1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map6) ).

cnf(map4,axiom,
    path(p0_1,s1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map4) ).

cnf(map2,axiom,
    path(p0_1,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map2) ).

cnf(map9,axiom,
    path(s2,p2_0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map9) ).

cnf(map7,axiom,
    path(s2,p1_2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map7) ).

cnf(map5,axiom,
    path(s1,p1_2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map5) ).

cnf(map3,axiom,
    path(s1,p0_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map3) ).

cnf(map11,axiom,
    path(s0,p2_0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map11) ).

cnf(map1,axiom,
    path(s0,p0_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map1) ).

cnf(map18,axiom,
    link(s2,s1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map18) ).

cnf(map14,axiom,
    link(s2,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map14) ).

cnf(map17,axiom,
    link(s1,s2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map17) ).

cnf(map15,axiom,
    link(s1,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map15) ).

cnf(map13,axiom,
    link(s0,s2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map13) ).

cnf(map16,axiom,
    link(s0,s1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',map16) ).

cnf(neq99,axiom,
    neq(p2_1,p2_0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq99) ).

cnf(neq98,axiom,
    neq(p2_1,p1_2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq98) ).

cnf(neq97,axiom,
    neq(p2_1,p0_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq97) ).

cnf(neq96,axiom,
    neq(p2_1,s2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq96) ).

cnf(neq95,axiom,
    neq(p2_1,s1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq95) ).

cnf(neq94,axiom,
    neq(p2_1,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq94) ).

cnf(neq93,axiom,
    neq(p2_1,truck3),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq93) ).

cnf(neq92,axiom,
    neq(p2_1,truck2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq92) ).

cnf(neq91,axiom,
    neq(p2_1,truck1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq91) ).

cnf(neq90,axiom,
    neq(p2_0,p2_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq90) ).

cnf(neq88,axiom,
    neq(p2_0,p1_2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq88) ).

cnf(neq87,axiom,
    neq(p2_0,p0_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq87) ).

cnf(neq86,axiom,
    neq(p2_0,s2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq86) ).

cnf(neq85,axiom,
    neq(p2_0,s1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq85) ).

cnf(neq84,axiom,
    neq(p2_0,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq84) ).

cnf(neq83,axiom,
    neq(p2_0,truck3),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq83) ).

cnf(neq82,axiom,
    neq(p2_0,truck2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq82) ).

cnf(neq81,axiom,
    neq(p2_0,truck1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq81) ).

cnf(neq80,axiom,
    neq(p1_2,p2_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq80) ).

cnf(neq79,axiom,
    neq(p1_2,p2_0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq79) ).

cnf(neq77,axiom,
    neq(p1_2,p0_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq77) ).

cnf(neq76,axiom,
    neq(p1_2,s2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq76) ).

cnf(neq75,axiom,
    neq(p1_2,s1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq75) ).

cnf(neq74,axiom,
    neq(p1_2,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq74) ).

cnf(neq73,axiom,
    neq(p1_2,truck3),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq73) ).

cnf(neq72,axiom,
    neq(p1_2,truck2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq72) ).

cnf(neq71,axiom,
    neq(p1_2,truck1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq71) ).

cnf(neq70,axiom,
    neq(p0_1,p2_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq70) ).

cnf(neq69,axiom,
    neq(p0_1,p2_0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq69) ).

cnf(neq68,axiom,
    neq(p0_1,p1_2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq68) ).

cnf(neq66,axiom,
    neq(p0_1,s2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq66) ).

cnf(neq65,axiom,
    neq(p0_1,s1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq65) ).

cnf(neq64,axiom,
    neq(p0_1,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq64) ).

cnf(neq63,axiom,
    neq(p0_1,truck3),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq63) ).

cnf(neq62,axiom,
    neq(p0_1,truck2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq62) ).

cnf(neq61,axiom,
    neq(p0_1,truck1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq61) ).

cnf(neq60,axiom,
    neq(s2,p2_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq60) ).

cnf(neq59,axiom,
    neq(s2,p2_0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq59) ).

cnf(neq58,axiom,
    neq(s2,p1_2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq58) ).

cnf(neq57,axiom,
    neq(s2,p0_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq57) ).

cnf(neq55,axiom,
    neq(s2,s1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq55) ).

cnf(neq54,axiom,
    neq(s2,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq54) ).

cnf(neq53,axiom,
    neq(s2,truck3),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq53) ).

cnf(neq52,axiom,
    neq(s2,truck2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq52) ).

cnf(neq51,axiom,
    neq(s2,truck1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq51) ).

cnf(neq50,axiom,
    neq(s1,p2_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq50) ).

cnf(neq49,axiom,
    neq(s1,p2_0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq49) ).

cnf(neq48,axiom,
    neq(s1,p1_2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq48) ).

cnf(neq47,axiom,
    neq(s1,p0_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq47) ).

cnf(neq46,axiom,
    neq(s1,s2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq46) ).

cnf(neq44,axiom,
    neq(s1,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq44) ).

cnf(neq43,axiom,
    neq(s1,truck3),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq43) ).

cnf(neq42,axiom,
    neq(s1,truck2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq42) ).

cnf(neq41,axiom,
    neq(s1,truck1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq41) ).

cnf(neq40,axiom,
    neq(s0,p2_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq40) ).

cnf(neq39,axiom,
    neq(s0,p2_0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq39) ).

cnf(neq38,axiom,
    neq(s0,p1_2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq38) ).

cnf(neq37,axiom,
    neq(s0,p0_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq37) ).

cnf(neq36,axiom,
    neq(s0,s2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq36) ).

cnf(neq35,axiom,
    neq(s0,s1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq35) ).

cnf(neq33,axiom,
    neq(s0,truck3),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq33) ).

cnf(neq32,axiom,
    neq(s0,truck2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq32) ).

cnf(neq31,axiom,
    neq(s0,truck1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq31) ).

cnf(neq30,axiom,
    neq(truck3,p2_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq30) ).

cnf(neq29,axiom,
    neq(truck3,p2_0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq29) ).

cnf(neq28,axiom,
    neq(truck3,p1_2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq28) ).

cnf(neq27,axiom,
    neq(truck3,p0_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq27) ).

cnf(neq26,axiom,
    neq(truck3,s2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq26) ).

cnf(neq25,axiom,
    neq(truck3,s1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq25) ).

cnf(neq24,axiom,
    neq(truck3,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq24) ).

cnf(neq22,axiom,
    neq(truck3,truck2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq22) ).

cnf(neq21,axiom,
    neq(truck3,truck1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq21) ).

cnf(neq20,axiom,
    neq(truck2,p2_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq20) ).

cnf(neq19,axiom,
    neq(truck2,p2_0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq19) ).

cnf(neq18,axiom,
    neq(truck2,p1_2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq18) ).

cnf(neq17,axiom,
    neq(truck2,p0_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq17) ).

cnf(neq16,axiom,
    neq(truck2,s2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq16) ).

cnf(neq15,axiom,
    neq(truck2,s1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq15) ).

cnf(neq14,axiom,
    neq(truck2,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq14) ).

cnf(neq13,axiom,
    neq(truck2,truck3),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq13) ).

cnf(neq11,axiom,
    neq(truck2,truck1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq11) ).

cnf(neq10,axiom,
    neq(truck1,p2_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq10) ).

cnf(neq9,axiom,
    neq(truck1,p2_0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq9) ).

cnf(neq8,axiom,
    neq(truck1,p1_2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq8) ).

cnf(neq7,axiom,
    neq(truck1,p0_1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq7) ).

cnf(neq6,axiom,
    neq(truck1,s2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq6) ).

cnf(neq5,axiom,
    neq(truck1,s1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq5) ).

cnf(neq4,axiom,
    neq(truck1,s0),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq4) ).

cnf(neq3,axiom,
    neq(truck1,truck3),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq3) ).

cnf(neq2,axiom,
    neq(truck1,truck2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',neq2) ).

cnf(i_0_186,axiom,
    ( s(X1,X2,X3,X4,X5,X6,truck3,X8,X9,X10,X11,X7)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X7)
    | ~ neq(X8,truck3)
    | ~ neq(X9,truck3) ),
    board5,
    [final] ).

cnf(i_0_187,axiom,
    ( s(X1,X2,X3,X4,X5,X6,truck2,X8,X9,X10,X7,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X7,X11)
    | ~ neq(X8,truck2)
    | ~ neq(X9,truck2) ),
    board3,
    [final] ).

cnf(i_0_188,axiom,
    ( s(X1,X2,X3,X4,X5,X6,truck1,X8,X9,X7,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X7,X10,X11)
    | ~ neq(X8,truck1)
    | ~ neq(X9,truck1) ),
    board1,
    [final] ).

cnf(i_0_189,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,truck3,X9,X10,X11,X8)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X8)
    | ~ neq(X7,truck3)
    | ~ neq(X9,truck3) ),
    board11,
    [final] ).

cnf(i_0_190,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,truck2,X9,X10,X8,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X8,X11)
    | ~ neq(X7,truck2)
    | ~ neq(X9,truck2) ),
    board9,
    [final] ).

cnf(i_0_191,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,truck1,X9,X8,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X8,X10,X11)
    | ~ neq(X7,truck1)
    | ~ neq(X9,truck1) ),
    board7,
    [final] ).

cnf(i_0_192,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,truck3,X10,X11,X9)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X9)
    | ~ neq(X7,truck3)
    | ~ neq(X8,truck3) ),
    board17,
    [final] ).

cnf(i_0_193,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,truck2,X10,X9,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X9,X11)
    | ~ neq(X7,truck2)
    | ~ neq(X8,truck2) ),
    board15,
    [final] ).

cnf(i_0_194,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,truck1,X9,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X9,X10,X11)
    | ~ neq(X7,truck1)
    | ~ neq(X8,truck1) ),
    board13,
    [final] ).

cnf(i_0_195,axiom,
    ( s(X1,X2,X3,X4,X5,X6,truck3,X7,X8,X9,X10,X12)
    | ~ s(X1,X2,X3,X4,X5,X6,truck3,X7,X8,X9,X10,X11)
    | ~ link(X11,X12) ),
    drive3,
    [final] ).

cnf(i_0_196,axiom,
    ( s(X1,X2,X3,X4,X5,X6,truck2,X7,X8,X9,X12,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,truck2,X7,X8,X9,X10,X11)
    | ~ link(X10,X12) ),
    drive2,
    [final] ).

cnf(i_0_197,axiom,
    ( s(X1,X2,X3,X4,X5,X6,truck1,X7,X8,X12,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,truck1,X7,X8,X9,X10,X11)
    | ~ link(X9,X12) ),
    drive1,
    [final] ).

cnf(i_0_198,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,truck3,X8,X9,X10,X12)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,truck3,X8,X9,X10,X11)
    | ~ link(X11,X12) ),
    drive6,
    [final] ).

cnf(i_0_199,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,truck2,X8,X9,X12,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,truck2,X8,X9,X10,X11)
    | ~ link(X10,X12) ),
    drive5,
    [final] ).

cnf(i_0_200,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,truck1,X8,X12,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,truck1,X8,X9,X10,X11)
    | ~ link(X9,X12) ),
    drive4,
    [final] ).

cnf(i_0_201,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,truck3,X9,X10,X12)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,truck3,X9,X10,X11)
    | ~ link(X11,X12) ),
    drive9,
    [final] ).

cnf(i_0_202,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,truck2,X9,X12,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,truck2,X9,X10,X11)
    | ~ link(X10,X12) ),
    drive8,
    [final] ).

cnf(i_0_203,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,truck1,X12,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,truck1,X9,X10,X11)
    | ~ link(X9,X12) ),
    drive7,
    [final] ).

cnf(i_0_204,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X13,X10,X11,X12)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
    | ~ path(X9,X13) ),
    walk3,
    [final] ).

cnf(i_0_205,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X13,X9,X10,X11,X12)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
    | ~ path(X8,X13) ),
    walk2,
    [final] ).

cnf(i_0_206,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X13,X8,X9,X10,X11,X12)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
    | ~ path(X7,X13) ),
    walk1,
    [final] ).

cnf(i_0_207,axiom,
    ( s(truck3,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1) ),
    load5,
    [final] ).

cnf(i_0_208,axiom,
    ( s(truck2,X2,X3,X4,X5,X6,X7,X8,X9,X10,X1,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X1,X11) ),
    load3,
    [final] ).

cnf(i_0_209,axiom,
    ( s(truck1,X2,X3,X4,X5,X6,X7,X8,X9,X1,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X1,X10,X11) ),
    load1,
    [final] ).

cnf(i_0_210,axiom,
    ( s(X1,truck3,X3,X4,X5,X6,X7,X8,X9,X10,X11,X2)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X2) ),
    load11,
    [final] ).

cnf(i_0_211,axiom,
    ( s(X1,truck2,X3,X4,X5,X6,X7,X8,X9,X10,X2,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X2,X11) ),
    load9,
    [final] ).

cnf(i_0_212,axiom,
    ( s(X1,truck1,X3,X4,X5,X6,X7,X8,X9,X2,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X2,X10,X11) ),
    load7,
    [final] ).

cnf(i_0_213,axiom,
    ( s(X1,X2,truck3,X4,X5,X6,X7,X8,X9,X10,X11,X3)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X3) ),
    load17,
    [final] ).

cnf(i_0_214,axiom,
    ( s(X1,X2,truck2,X4,X5,X6,X7,X8,X9,X10,X3,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X3,X11) ),
    load15,
    [final] ).

cnf(i_0_215,axiom,
    ( s(X1,X2,truck1,X4,X5,X6,X7,X8,X9,X3,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X3,X10,X11) ),
    load13,
    [final] ).

cnf(i_0_216,axiom,
    ( s(X1,X2,X3,truck3,X5,X6,X7,X8,X9,X10,X11,X4)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X4) ),
    load23,
    [final] ).

cnf(i_0_217,axiom,
    ( s(X1,X2,X3,truck2,X5,X6,X7,X8,X9,X10,X4,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X4,X11) ),
    load21,
    [final] ).

cnf(i_0_218,axiom,
    ( s(X1,X2,X3,truck1,X5,X6,X7,X8,X9,X4,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X4,X10,X11) ),
    load19,
    [final] ).

cnf(i_0_219,axiom,
    ( s(X1,X2,X3,X4,truck3,X6,X7,X8,X9,X10,X11,X5)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X5) ),
    load29,
    [final] ).

cnf(i_0_220,axiom,
    ( s(X1,X2,X3,X4,truck2,X6,X7,X8,X9,X10,X5,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X5,X11) ),
    load27,
    [final] ).

cnf(i_0_221,axiom,
    ( s(X1,X2,X3,X4,truck1,X6,X7,X8,X9,X5,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X5,X10,X11) ),
    load25,
    [final] ).

cnf(i_0_222,axiom,
    ( s(X1,X2,X3,X4,X5,truck3,X7,X8,X9,X10,X11,X6)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X6) ),
    load35,
    [final] ).

cnf(i_0_223,axiom,
    ( s(X1,X2,X3,X4,X5,truck2,X7,X8,X9,X10,X6,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X6,X11) ),
    load33,
    [final] ).

cnf(i_0_224,axiom,
    ( s(X1,X2,X3,X4,X5,truck1,X7,X8,X9,X6,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X6,X10,X11) ),
    load31,
    [final] ).

cnf(i_0_225,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X1,X10,X11)
    | ~ s(truck1,X2,X3,X4,X5,X6,X7,X8,X9,X1,X10,X11) ),
    load2,
    [final] ).

cnf(i_0_226,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X1,X11)
    | ~ s(truck2,X2,X3,X4,X5,X6,X7,X8,X9,X10,X1,X11) ),
    load4,
    [final] ).

cnf(i_0_227,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1)
    | ~ s(truck3,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1) ),
    load6,
    [final] ).

cnf(i_0_228,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X2,X10,X11)
    | ~ s(X1,truck1,X3,X4,X5,X6,X7,X8,X9,X2,X10,X11) ),
    load8,
    [final] ).

cnf(i_0_229,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X2,X11)
    | ~ s(X1,truck2,X3,X4,X5,X6,X7,X8,X9,X10,X2,X11) ),
    load10,
    [final] ).

cnf(i_0_230,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X2)
    | ~ s(X1,truck3,X3,X4,X5,X6,X7,X8,X9,X10,X11,X2) ),
    load12,
    [final] ).

cnf(i_0_231,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X3,X10,X11)
    | ~ s(X1,X2,truck1,X4,X5,X6,X7,X8,X9,X3,X10,X11) ),
    load14,
    [final] ).

cnf(i_0_232,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X3,X11)
    | ~ s(X1,X2,truck2,X4,X5,X6,X7,X8,X9,X10,X3,X11) ),
    load16,
    [final] ).

cnf(i_0_233,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X3)
    | ~ s(X1,X2,truck3,X4,X5,X6,X7,X8,X9,X10,X11,X3) ),
    load18,
    [final] ).

cnf(i_0_234,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X4,X10,X11)
    | ~ s(X1,X2,X3,truck1,X5,X6,X7,X8,X9,X4,X10,X11) ),
    load20,
    [final] ).

cnf(i_0_235,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X4,X11)
    | ~ s(X1,X2,X3,truck2,X5,X6,X7,X8,X9,X10,X4,X11) ),
    load22,
    [final] ).

cnf(i_0_236,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X4)
    | ~ s(X1,X2,X3,truck3,X5,X6,X7,X8,X9,X10,X11,X4) ),
    load24,
    [final] ).

cnf(i_0_237,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X5,X10,X11)
    | ~ s(X1,X2,X3,X4,truck1,X6,X7,X8,X9,X5,X10,X11) ),
    load26,
    [final] ).

cnf(i_0_238,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X5,X11)
    | ~ s(X1,X2,X3,X4,truck2,X6,X7,X8,X9,X10,X5,X11) ),
    load28,
    [final] ).

cnf(i_0_239,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X5)
    | ~ s(X1,X2,X3,X4,truck3,X6,X7,X8,X9,X10,X11,X5) ),
    load30,
    [final] ).

cnf(i_0_240,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X6,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,truck1,X7,X8,X9,X6,X10,X11) ),
    load32,
    [final] ).

cnf(i_0_241,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X6,X11)
    | ~ s(X1,X2,X3,X4,X5,truck2,X7,X8,X9,X10,X6,X11) ),
    load34,
    [final] ).

cnf(i_0_242,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X6)
    | ~ s(X1,X2,X3,X4,X5,truck3,X7,X8,X9,X10,X11,X6) ),
    load36,
    [final] ).

cnf(i_0_243,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X7,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,truck1,X8,X9,X7,X10,X11) ),
    board2,
    [final] ).

cnf(i_0_244,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X7,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,truck2,X8,X9,X10,X7,X11) ),
    board4,
    [final] ).

cnf(i_0_245,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X7)
    | ~ s(X1,X2,X3,X4,X5,X6,truck3,X8,X9,X10,X11,X7) ),
    board6,
    [final] ).

cnf(i_0_246,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X8,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,truck1,X9,X8,X10,X11) ),
    board8,
    [final] ).

cnf(i_0_247,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X8,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,truck2,X9,X10,X8,X11) ),
    board10,
    [final] ).

cnf(i_0_248,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X8)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,truck3,X9,X10,X11,X8) ),
    board12,
    [final] ).

cnf(i_0_249,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X9,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,truck1,X9,X10,X11) ),
    board14,
    [final] ).

cnf(i_0_250,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X9,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,truck2,X10,X9,X11) ),
    board16,
    [final] ).

cnf(i_0_251,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X9)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,truck3,X10,X11,X9) ),
    board18,
    [final] ).

cnf(i_0_252,negated_conjecture,
    ~ s(s0,s1,s1,s1,s2,s2,s0,s2,X1,s1,s0,s0),
    goal,
    [final] ).

cnf(i_0_253,axiom,
    s(s2,s0,s1,s1,s2,s1,s0,s0,s1,s1,s0,s0),
    init,
    [final] ).

cnf(i_0_254,axiom,
    ~ neq(p2_1,p2_1),
    neq100,
    [final] ).

cnf(i_0_255,axiom,
    ~ neq(p2_0,p2_0),
    neq89,
    [final] ).

cnf(i_0_256,axiom,
    ~ neq(p1_2,p1_2),
    neq78,
    [final] ).

cnf(i_0_257,axiom,
    ~ neq(p0_1,p0_1),
    neq67,
    [final] ).

cnf(i_0_258,axiom,
    ~ neq(s2,s2),
    neq56,
    [final] ).

cnf(i_0_259,axiom,
    ~ neq(s1,s1),
    neq45,
    [final] ).

cnf(i_0_260,axiom,
    ~ neq(s0,s0),
    neq34,
    [final] ).

cnf(i_0_261,axiom,
    ~ neq(truck3,truck3),
    neq23,
    [final] ).

cnf(i_0_262,axiom,
    ~ neq(truck2,truck2),
    neq12,
    [final] ).

cnf(i_0_263,axiom,
    ~ neq(truck1,truck1),
    neq1,
    [final] ).

cnf(i_0_264,axiom,
    path(p2_0,s2),
    map10,
    [final] ).

cnf(i_0_265,axiom,
    path(p2_0,s0),
    map12,
    [final] ).

cnf(i_0_266,axiom,
    path(p1_2,s2),
    map8,
    [final] ).

cnf(i_0_267,axiom,
    path(p1_2,s1),
    map6,
    [final] ).

cnf(i_0_268,axiom,
    path(p0_1,s1),
    map4,
    [final] ).

cnf(i_0_269,axiom,
    path(p0_1,s0),
    map2,
    [final] ).

cnf(i_0_270,axiom,
    path(s2,p2_0),
    map9,
    [final] ).

cnf(i_0_271,axiom,
    path(s2,p1_2),
    map7,
    [final] ).

cnf(i_0_272,axiom,
    path(s1,p1_2),
    map5,
    [final] ).

cnf(i_0_273,axiom,
    path(s1,p0_1),
    map3,
    [final] ).

cnf(i_0_274,axiom,
    path(s0,p2_0),
    map11,
    [final] ).

cnf(i_0_275,axiom,
    path(s0,p0_1),
    map1,
    [final] ).

cnf(i_0_276,axiom,
    link(s2,s1),
    map18,
    [final] ).

cnf(i_0_277,axiom,
    link(s2,s0),
    map14,
    [final] ).

cnf(i_0_278,axiom,
    link(s1,s2),
    map17,
    [final] ).

cnf(i_0_279,axiom,
    link(s1,s0),
    map15,
    [final] ).

cnf(i_0_280,axiom,
    link(s0,s2),
    map13,
    [final] ).

cnf(i_0_281,axiom,
    link(s0,s1),
    map16,
    [final] ).

cnf(i_0_282,axiom,
    neq(p2_1,p2_0),
    neq99,
    [final] ).

cnf(i_0_283,axiom,
    neq(p2_1,p1_2),
    neq98,
    [final] ).

cnf(i_0_284,axiom,
    neq(p2_1,p0_1),
    neq97,
    [final] ).

cnf(i_0_285,axiom,
    neq(p2_1,s2),
    neq96,
    [final] ).

cnf(i_0_286,axiom,
    neq(p2_1,s1),
    neq95,
    [final] ).

cnf(i_0_287,axiom,
    neq(p2_1,s0),
    neq94,
    [final] ).

cnf(i_0_288,axiom,
    neq(p2_1,truck3),
    neq93,
    [final] ).

cnf(i_0_289,axiom,
    neq(p2_1,truck2),
    neq92,
    [final] ).

cnf(i_0_290,axiom,
    neq(p2_1,truck1),
    neq91,
    [final] ).

cnf(i_0_291,axiom,
    neq(p2_0,p2_1),
    neq90,
    [final] ).

cnf(i_0_292,axiom,
    neq(p2_0,p1_2),
    neq88,
    [final] ).

cnf(i_0_293,axiom,
    neq(p2_0,p0_1),
    neq87,
    [final] ).

cnf(i_0_294,axiom,
    neq(p2_0,s2),
    neq86,
    [final] ).

cnf(i_0_295,axiom,
    neq(p2_0,s1),
    neq85,
    [final] ).

cnf(i_0_296,axiom,
    neq(p2_0,s0),
    neq84,
    [final] ).

cnf(i_0_297,axiom,
    neq(p2_0,truck3),
    neq83,
    [final] ).

cnf(i_0_298,axiom,
    neq(p2_0,truck2),
    neq82,
    [final] ).

cnf(i_0_299,axiom,
    neq(p2_0,truck1),
    neq81,
    [final] ).

cnf(i_0_300,axiom,
    neq(p1_2,p2_1),
    neq80,
    [final] ).

cnf(i_0_301,axiom,
    neq(p1_2,p2_0),
    neq79,
    [final] ).

cnf(i_0_302,axiom,
    neq(p1_2,p0_1),
    neq77,
    [final] ).

cnf(i_0_303,axiom,
    neq(p1_2,s2),
    neq76,
    [final] ).

cnf(i_0_304,axiom,
    neq(p1_2,s1),
    neq75,
    [final] ).

cnf(i_0_305,axiom,
    neq(p1_2,s0),
    neq74,
    [final] ).

cnf(i_0_306,axiom,
    neq(p1_2,truck3),
    neq73,
    [final] ).

cnf(i_0_307,axiom,
    neq(p1_2,truck2),
    neq72,
    [final] ).

cnf(i_0_308,axiom,
    neq(p1_2,truck1),
    neq71,
    [final] ).

cnf(i_0_309,axiom,
    neq(p0_1,p2_1),
    neq70,
    [final] ).

cnf(i_0_310,axiom,
    neq(p0_1,p2_0),
    neq69,
    [final] ).

cnf(i_0_311,axiom,
    neq(p0_1,p1_2),
    neq68,
    [final] ).

cnf(i_0_312,axiom,
    neq(p0_1,s2),
    neq66,
    [final] ).

cnf(i_0_313,axiom,
    neq(p0_1,s1),
    neq65,
    [final] ).

cnf(i_0_314,axiom,
    neq(p0_1,s0),
    neq64,
    [final] ).

cnf(i_0_315,axiom,
    neq(p0_1,truck3),
    neq63,
    [final] ).

cnf(i_0_316,axiom,
    neq(p0_1,truck2),
    neq62,
    [final] ).

cnf(i_0_317,axiom,
    neq(p0_1,truck1),
    neq61,
    [final] ).

cnf(i_0_318,axiom,
    neq(s2,p2_1),
    neq60,
    [final] ).

cnf(i_0_319,axiom,
    neq(s2,p2_0),
    neq59,
    [final] ).

cnf(i_0_320,axiom,
    neq(s2,p1_2),
    neq58,
    [final] ).

cnf(i_0_321,axiom,
    neq(s2,p0_1),
    neq57,
    [final] ).

cnf(i_0_322,axiom,
    neq(s2,s1),
    neq55,
    [final] ).

cnf(i_0_323,axiom,
    neq(s2,s0),
    neq54,
    [final] ).

cnf(i_0_324,axiom,
    neq(s2,truck3),
    neq53,
    [final] ).

cnf(i_0_325,axiom,
    neq(s2,truck2),
    neq52,
    [final] ).

cnf(i_0_326,axiom,
    neq(s2,truck1),
    neq51,
    [final] ).

cnf(i_0_327,axiom,
    neq(s1,p2_1),
    neq50,
    [final] ).

cnf(i_0_328,axiom,
    neq(s1,p2_0),
    neq49,
    [final] ).

cnf(i_0_329,axiom,
    neq(s1,p1_2),
    neq48,
    [final] ).

cnf(i_0_330,axiom,
    neq(s1,p0_1),
    neq47,
    [final] ).

cnf(i_0_331,axiom,
    neq(s1,s2),
    neq46,
    [final] ).

cnf(i_0_332,axiom,
    neq(s1,s0),
    neq44,
    [final] ).

cnf(i_0_333,axiom,
    neq(s1,truck3),
    neq43,
    [final] ).

cnf(i_0_334,axiom,
    neq(s1,truck2),
    neq42,
    [final] ).

cnf(i_0_335,axiom,
    neq(s1,truck1),
    neq41,
    [final] ).

cnf(i_0_336,axiom,
    neq(s0,p2_1),
    neq40,
    [final] ).

cnf(i_0_337,axiom,
    neq(s0,p2_0),
    neq39,
    [final] ).

cnf(i_0_338,axiom,
    neq(s0,p1_2),
    neq38,
    [final] ).

cnf(i_0_339,axiom,
    neq(s0,p0_1),
    neq37,
    [final] ).

cnf(i_0_340,axiom,
    neq(s0,s2),
    neq36,
    [final] ).

cnf(i_0_341,axiom,
    neq(s0,s1),
    neq35,
    [final] ).

cnf(i_0_342,axiom,
    neq(s0,truck3),
    neq33,
    [final] ).

cnf(i_0_343,axiom,
    neq(s0,truck2),
    neq32,
    [final] ).

cnf(i_0_344,axiom,
    neq(s0,truck1),
    neq31,
    [final] ).

cnf(i_0_345,axiom,
    neq(truck3,p2_1),
    neq30,
    [final] ).

cnf(i_0_346,axiom,
    neq(truck3,p2_0),
    neq29,
    [final] ).

cnf(i_0_347,axiom,
    neq(truck3,p1_2),
    neq28,
    [final] ).

cnf(i_0_348,axiom,
    neq(truck3,p0_1),
    neq27,
    [final] ).

cnf(i_0_349,axiom,
    neq(truck3,s2),
    neq26,
    [final] ).

cnf(i_0_350,axiom,
    neq(truck3,s1),
    neq25,
    [final] ).

cnf(i_0_351,axiom,
    neq(truck3,s0),
    neq24,
    [final] ).

cnf(i_0_352,axiom,
    neq(truck3,truck2),
    neq22,
    [final] ).

cnf(i_0_353,axiom,
    neq(truck3,truck1),
    neq21,
    [final] ).

cnf(i_0_354,axiom,
    neq(truck2,p2_1),
    neq20,
    [final] ).

cnf(i_0_355,axiom,
    neq(truck2,p2_0),
    neq19,
    [final] ).

cnf(i_0_356,axiom,
    neq(truck2,p1_2),
    neq18,
    [final] ).

cnf(i_0_357,axiom,
    neq(truck2,p0_1),
    neq17,
    [final] ).

cnf(i_0_358,axiom,
    neq(truck2,s2),
    neq16,
    [final] ).

cnf(i_0_359,axiom,
    neq(truck2,s1),
    neq15,
    [final] ).

cnf(i_0_360,axiom,
    neq(truck2,s0),
    neq14,
    [final] ).

cnf(i_0_361,axiom,
    neq(truck2,truck3),
    neq13,
    [final] ).

cnf(i_0_362,axiom,
    neq(truck2,truck1),
    neq11,
    [final] ).

cnf(i_0_363,axiom,
    neq(truck1,p2_1),
    neq10,
    [final] ).

cnf(i_0_364,axiom,
    neq(truck1,p2_0),
    neq9,
    [final] ).

cnf(i_0_365,axiom,
    neq(truck1,p1_2),
    neq8,
    [final] ).

cnf(i_0_366,axiom,
    neq(truck1,p0_1),
    neq7,
    [final] ).

cnf(i_0_367,axiom,
    neq(truck1,s2),
    neq6,
    [final] ).

cnf(i_0_368,axiom,
    neq(truck1,s1),
    neq5,
    [final] ).

cnf(i_0_369,axiom,
    neq(truck1,s0),
    neq4,
    [final] ).

cnf(i_0_370,axiom,
    neq(truck1,truck3),
    neq3,
    [final] ).

cnf(i_0_371,axiom,
    neq(truck1,truck2),
    neq2,
    [final] ).

cnf(i_0_4237,plain,
    ~ s(s0,truck3,truck3,truck3,s2,s2,p1_2,s2,truck3,s1,s0,s1),
    inference(scs_inference,[],[i_0_4177,i_0_4005,i_0_4231,i_0_3637,i_0_244,i_0_251]) ).

cnf(i_0_4239,plain,
    ~ s(s0,s1,s1,s1,s2,s2,s0,truck1,s1,s1,s1,s0),
    inference(scs_inference,[],[i_0_4177,i_0_4005,i_0_4231,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246]) ).

cnf(i_0_4241,plain,
    ~ s(truck1,s1,s1,s1,s2,s2,truck1,p0_1,truck2,s0,s0,s0),
    inference(scs_inference,[],[i_0_4177,i_0_4005,i_0_4231,i_0_3841,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243]) ).

cnf(i_0_4243,plain,
    s(truck3,s0,truck3,truck3,truck3,s1,s0,truck3,s1,s1,s0,s1),
    inference(scs_inference,[],[i_0_4177,i_0_4005,i_0_4231,i_0_3841,i_0_4015,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213]) ).

cnf(i_0_4245,plain,
    s(truck3,s0,s1,truck3,truck3,truck3,s0,truck3,s1,s1,s0,s1),
    inference(scs_inference,[],[i_0_4177,i_0_4005,i_0_4231,i_0_3841,i_0_4015,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222]) ).

cnf(i_0_4247,plain,
    ~ s(s0,s1,s1,s1,s2,s2,truck3,p2_0,s1,s1,s1,s0),
    inference(scs_inference,[],[i_0_4177,i_0_3621,i_0_4005,i_0_4231,i_0_3841,i_0_4015,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245]) ).

cnf(i_0_4249,plain,
    s(truck3,truck3,s1,truck3,s2,s1,truck3,s0,truck1,s1,s0,s1),
    inference(scs_inference,[],[i_0_4177,i_0_3621,i_0_4005,i_0_4231,i_0_3841,i_0_4015,i_0_4093,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216]) ).

cnf(i_0_4251,plain,
    s(truck1,truck3,s1,s1,truck2,s1,s0,truck2,truck1,s2,s2,s0),
    inference(scs_inference,[],[i_0_3933,i_0_4177,i_0_3621,i_0_4005,i_0_4231,i_0_3841,i_0_4015,i_0_4093,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210]) ).

cnf(i_0_4253,plain,
    s(s2,s0,truck2,s1,truck2,truck2,s0,truck2,truck1,s1,s1,s0),
    inference(scs_inference,[],[i_0_3933,i_0_4177,i_0_3621,i_0_4005,i_0_4231,i_0_3841,i_0_4015,i_0_4021,i_0_4093,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223]) ).

cnf(i_0_4255,plain,
    s(s2,s0,truck2,truck2,truck2,s1,s0,truck2,truck1,s1,s1,s0),
    inference(scs_inference,[],[i_0_3933,i_0_4177,i_0_3621,i_0_4005,i_0_4231,i_0_3841,i_0_4015,i_0_4021,i_0_4025,i_0_4093,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214]) ).

cnf(i_0_4257,plain,
    s(s2,s0,s1,truck2,truck2,truck2,s0,truck2,truck1,s1,s1,s0),
    inference(scs_inference,[],[i_0_3933,i_0_4177,i_0_3621,i_0_4005,i_0_4231,i_0_3841,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217]) ).

cnf(i_0_4259,plain,
    ~ s(s0,s1,s1,s1,s2,s2,s0,truck2,s1,s1,s1,s0),
    inference(scs_inference,[],[i_0_3933,i_0_4177,i_0_3621,i_0_4005,i_0_4231,i_0_3841,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247]) ).

cnf(i_0_4261,plain,
    s(truck1,truck2,s1,s1,truck1,s1,s0,p0_1,truck1,s2,s0,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_4005,i_0_4231,i_0_3841,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211]) ).

cnf(i_0_4263,plain,
    s(truck2,truck3,s1,truck2,truck2,s1,truck2,s0,truck1,s1,s2,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_4005,i_0_4231,i_0_3841,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4205,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208]) ).

cnf(i_0_4265,plain,
    ~ s(s0,s1,s1,s1,truck3,truck3,p1_2,truck3,truck3,s1,s0,s2),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_4005,i_0_4231,i_0_3841,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4205,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248]) ).

cnf(i_0_4267,plain,
    ~ s(s0,truck3,truck3,truck3,s2,s2,p1_2,s2,truck1,s1,s0,s1),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_4005,i_0_4231,i_0_3841,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4205,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249]) ).

cnf(i_0_4269,plain,
    s(s2,truck2,truck1,truck1,s2,s1,s0,s0,truck1,s1,s0,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_4005,i_0_4231,i_0_3841,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4205,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218]) ).

cnf(i_0_4271,plain,
    s(s2,truck2,truck1,s1,s2,truck1,s0,s0,truck1,s1,s0,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_4005,i_0_4231,i_0_3841,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4205,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224]) ).

cnf(i_0_4273,plain,
    s(s2,truck3,truck1,s1,s2,truck1,s0,s0,truck1,s1,s0,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_4005,i_0_4231,i_0_3841,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4205,i_0_4224,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215]) ).

cnf(i_0_4275,plain,
    s(s2,truck3,truck1,s1,truck1,s1,s0,s0,truck1,s2,s0,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_4005,i_0_4231,i_0_3841,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221]) ).

cnf(i_0_4277,plain,
    ~ s(s0,s1,s1,s1,truck2,truck2,p2_0,s2,truck2,s1,s2,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250]) ).

cnf(i_0_4279,plain,
    ~ s(s0,s1,s1,s1,truck1,truck1,truck1,truck1,s2,s2,s0,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237]) ).

cnf(i_0_4281,plain,
    ~ s(truck1,s1,s1,s1,s2,s2,truck1,p0_1,s0,s0,s0,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225]) ).

cnf(i_0_4283,plain,
    ~ s(s0,s1,s1,s1,s2,truck1,p0_1,truck1,truck1,s2,s0,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4119,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240]) ).

cnf(i_0_4285,plain,
    ~ s(s0,s1,s1,s1,truck3,truck3,s0,truck1,s2,s1,s0,s2),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4119,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239]) ).

cnf(i_0_4287,plain,
    ~ s(s0,truck1,s1,s1,s2,s2,s0,p2_0,s1,s1,s1,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4119,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228]) ).

cnf(i_0_4289,plain,
    ~ s(s0,s1,s1,truck1,s2,s2,s0,p2_0,s1,s1,s1,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4093,i_0_4119,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234]) ).

cnf(i_0_4291,plain,
    ~ s(s0,truck3,truck3,s1,s2,s2,s0,p2_0,truck1,s1,s0,s1),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4119,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230]) ).

cnf(i_0_4293,plain,
    ~ s(s0,s1,truck1,s1,s2,s2,s0,p2_0,s1,s1,s1,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4119,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231]) ).

cnf(i_0_4295,plain,
    ~ s(truck3,s1,s1,s1,s2,s2,s0,p2_0,s1,s1,s1,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4119,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227]) ).

cnf(i_0_4297,plain,
    ~ s(s0,s1,truck3,truck3,s2,s2,s0,p2_0,truck1,s1,s0,s1),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4119,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236]) ).

cnf(i_0_4299,plain,
    ~ s(s0,s1,truck3,truck3,s2,s2,s0,p2_0,p0_1,s1,s0,s1),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4119,i_0_4179,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233]) ).

cnf(i_0_4301,plain,
    ~ s(s0,s1,s1,s1,s2,truck3,s1,s2,s2,s1,s0,s2),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4179,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242]) ).

cnf(i_0_4303,plain,
    ~ s(s0,truck2,s1,s1,s2,s2,s0,p2_0,s1,s1,s1,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4179,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229]) ).

cnf(i_0_4305,plain,
    ~ s(s0,s1,s1,truck2,s2,s2,s0,p2_0,s1,s1,s1,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4179,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235]) ).

cnf(i_0_4307,plain,
    ~ s(s0,s1,truck2,s1,s2,s2,s0,p2_0,s1,s1,s1,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4179,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232]) ).

cnf(i_0_4309,plain,
    ~ s(s0,s1,s1,s1,truck2,s2,s1,truck2,truck2,s1,s2,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238]) ).

cnf(i_0_4311,plain,
    ~ s(s0,s1,s1,truck1,truck2,truck2,p2_0,truck2,s2,s1,s2,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_3947,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241]) ).

cnf(i_0_4313,plain,
    ~ s(truck2,truck3,truck3,truck3,s2,s2,p1_2,s2,s1,s1,s0,s1),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_3947,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_3989,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226]) ).

cnf(i_0_4315,plain,
    ~ s(s0,truck3,truck3,truck3,s2,s2,p1_2,s2,p1_2,s1,s0,s1),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3841,i_0_3941,i_0_3947,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_3989,i_0_267,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204]) ).

cnf(i_0_4317,plain,
    s(s2,truck3,s1,s1,s2,s1,s0,truck3,truck1,s1,s0,s1),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3777,i_0_3841,i_0_3941,i_0_3947,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_3989,i_0_267,i_0_281,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198]) ).

cnf(i_0_4319,plain,
    s(s2,s0,s1,s1,s2,s1,s0,truck2,s1,s1,s1,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3777,i_0_3841,i_0_3941,i_0_3947,i_0_3993,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_3989,i_0_267,i_0_281,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199]) ).

cnf(i_0_4321,plain,
    s(truck1,truck3,s1,s1,truck1,s1,truck2,s0,truck1,s2,s1,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3777,i_0_3841,i_0_3941,i_0_3947,i_0_3993,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_3989,i_0_267,i_0_281,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196]) ).

cnf(i_0_4323,plain,
    s(truck3,truck3,s1,s1,truck3,s1,truck3,s0,truck1,s1,s0,s0),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3777,i_0_3841,i_0_3941,i_0_3947,i_0_3993,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_4017,i_0_3989,i_0_267,i_0_281,i_0_277,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195]) ).

cnf(i_0_4325,plain,
    ~ s(s0,truck3,truck3,truck3,s2,s2,p1_2,p2_0,s1,s1,s0,s1),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3777,i_0_3841,i_0_3941,i_0_3947,i_0_3993,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_4017,i_0_3989,i_0_267,i_0_264,i_0_281,i_0_277,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205]) ).

cnf(i_0_4327,plain,
    ~ s(s0,truck3,truck3,truck3,s2,s2,s2,s2,s1,s1,s0,s1),
    inference(scs_inference,[],[i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3777,i_0_3841,i_0_3941,i_0_3947,i_0_3993,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_4017,i_0_3989,i_0_271,i_0_267,i_0_264,i_0_281,i_0_277,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205,i_0_206]) ).

cnf(i_0_4329,plain,
    s(truck1,truck2,s1,s1,truck1,s1,s0,s0,truck1,s0,s0,s0),
    inference(scs_inference,[],[i_0_3811,i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3777,i_0_3841,i_0_3941,i_0_3947,i_0_3993,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_4017,i_0_3989,i_0_271,i_0_267,i_0_264,i_0_281,i_0_277,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205,i_0_206,i_0_203]) ).

cnf(i_0_4331,plain,
    ~ s(s0,truck3,truck3,s1,s2,s2,s1,s2,s0,s1,s0,s1),
    inference(scs_inference,[],[i_0_3811,i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3777,i_0_3841,i_0_3941,i_0_3947,i_0_3993,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_4228,i_0_4017,i_0_3989,i_0_271,i_0_267,i_0_264,i_0_281,i_0_334,i_0_277,i_0_325,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205,i_0_206,i_0_203,i_0_193]) ).

cnf(i_0_4333,plain,
    s(truck1,truck2,s1,s1,truck1,s1,s0,truck3,truck1,s2,s0,s0),
    inference(scs_inference,[],[i_0_3811,i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3777,i_0_3841,i_0_3941,i_0_3947,i_0_3993,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_4228,i_0_4017,i_0_3989,i_0_271,i_0_267,i_0_264,i_0_281,i_0_334,i_0_277,i_0_342,i_0_370,i_0_325,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205,i_0_206,i_0_203,i_0_193,i_0_189]) ).

cnf(i_0_4335,plain,
    s(truck1,truck2,s1,s1,truck1,s1,s0,truck2,truck1,s2,s0,s0),
    inference(scs_inference,[],[i_0_3811,i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3777,i_0_3841,i_0_3941,i_0_3947,i_0_3993,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_4228,i_0_4017,i_0_3989,i_0_271,i_0_267,i_0_264,i_0_281,i_0_334,i_0_277,i_0_342,i_0_371,i_0_343,i_0_370,i_0_325,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205,i_0_206,i_0_203,i_0_193,i_0_189,i_0_190]) ).

cnf(i_0_4337,plain,
    ~ s(s0,s1,truck3,s1,s2,s2,s0,p2_0,s1,s1,s0,s1),
    inference(scs_inference,[],[i_0_3811,i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3777,i_0_3841,i_0_3941,i_0_3947,i_0_3993,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_4228,i_0_4017,i_0_3989,i_0_271,i_0_267,i_0_264,i_0_299,i_0_281,i_0_334,i_0_277,i_0_342,i_0_371,i_0_343,i_0_370,i_0_344,i_0_325,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205,i_0_206,i_0_203,i_0_193,i_0_189,i_0_190,i_0_194]) ).

cnf(i_0_4339,plain,
    s(truck1,truck2,s1,s1,truck1,s1,truck3,s0,truck1,s2,s0,s0),
    inference(scs_inference,[],[i_0_3811,i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3777,i_0_3841,i_0_3941,i_0_3947,i_0_3993,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_4228,i_0_4017,i_0_3989,i_0_271,i_0_267,i_0_264,i_0_299,i_0_281,i_0_334,i_0_277,i_0_342,i_0_371,i_0_343,i_0_370,i_0_344,i_0_325,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205,i_0_206,i_0_203,i_0_193,i_0_189,i_0_190,i_0_194,i_0_186]) ).

cnf(i_0_4343,plain,
    ~ s(s0,s1,s1,s1,s2,s2,s0,s2,s2,s1,s0,s2),
    inference(scs_inference,[],[i_0_3811,i_0_3933,i_0_3997,i_0_4177,i_0_3621,i_0_3678,i_0_3692,i_0_3995,i_0_4005,i_0_4081,i_0_4231,i_0_3777,i_0_3841,i_0_3941,i_0_3947,i_0_3993,i_0_4003,i_0_4015,i_0_4021,i_0_4023,i_0_4025,i_0_4069,i_0_4093,i_0_4105,i_0_4119,i_0_4141,i_0_4179,i_0_4205,i_0_4224,i_0_4228,i_0_372,i_0_4017,i_0_3989,i_0_271,i_0_267,i_0_264,i_0_299,i_0_281,i_0_334,i_0_277,i_0_342,i_0_371,i_0_343,i_0_370,i_0_344,i_0_324,i_0_325,i_0_3637,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_221,i_0_250,i_0_237,i_0_225,i_0_240,i_0_239,i_0_228,i_0_234,i_0_230,i_0_231,i_0_227,i_0_236,i_0_233,i_0_242,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205,i_0_206,i_0_203,i_0_193,i_0_189,i_0_190,i_0_194,i_0_186,i_0_191,i_0_192]) ).

cnf(i_0_4353,plain,
    s(s2,truck3,truck3,s1,truck3,truck3,truck3,s0,truck1,s1,s0,s1),
    inference(scs_inference,[],[i_0_4051,i_0_3591,i_0_3957,i_0_4125,i_0_1035,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213]) ).

cnf(i_0_4355,plain,
    s(s2,truck3,s1,truck3,truck3,truck3,truck3,s0,truck1,s1,s0,s1),
    inference(scs_inference,[],[i_0_4051,i_0_3591,i_0_3957,i_0_4125,i_0_4129,i_0_1035,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222]) ).

cnf(i_0_4357,plain,
    ~ s(s0,s1,s1,s1,truck1,truck1,truck3,p1_2,s2,s2,s0,s0),
    inference(scs_inference,[],[i_0_4051,i_0_3591,i_0_3957,i_0_4125,i_0_4129,i_0_1035,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245]) ).

cnf(i_0_4359,plain,
    s(truck3,s0,s1,truck3,truck3,s1,s0,truck3,truck1,s1,s0,s1),
    inference(scs_inference,[],[i_0_4051,i_0_3591,i_0_3957,i_0_4125,i_0_4129,i_0_4201,i_0_1035,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216]) ).

cnf(i_0_4361,plain,
    s(truck1,truck3,s1,s1,truck1,s1,p0_1,s0,truck1,s2,s0,s0),
    inference(scs_inference,[],[i_0_4051,i_0_4045,i_0_3591,i_0_3957,i_0_4125,i_0_4129,i_0_4201,i_0_1035,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210]) ).

cnf(i_0_4573,plain,
    ~ s(s0,s1,s1,s1,truck3,truck3,s0,p0_1,truck3,s1,s0,s2),
    inference(scs_inference,[],[i_0_3973,i_0_4185,i_0_244,i_0_251]) ).

cnf(i_0_4575,plain,
    ~ s(s0,s1,s1,s1,s2,s2,p2_0,truck1,truck1,s2,s0,s0),
    inference(scs_inference,[],[i_0_3973,i_0_4185,i_0_1244,i_0_244,i_0_251,i_0_246]) ).

cnf(i_0_4363,plain,
    s(s2,s0,truck2,truck2,truck2,truck2,s0,truck2,truck1,s1,s1,s0),
    inference(scs_inference,[],[i_0_4051,i_0_4045,i_0_4255,i_0_3591,i_0_3957,i_0_4125,i_0_4129,i_0_4201,i_0_1035,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223]) ).

cnf(i_0_4365,plain,
    s(s2,truck3,truck2,truck2,truck2,truck2,truck2,s0,truck1,s1,s1,s0),
    inference(scs_inference,[],[i_0_4051,i_0_4045,i_0_4255,i_0_3591,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4201,i_0_1035,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214]) ).

cnf(i_0_4367,plain,
    s(truck2,truck3,s1,truck2,truck2,s1,s0,truck2,truck1,s1,s1,s0),
    inference(scs_inference,[],[i_0_4051,i_0_4045,i_0_4255,i_0_3591,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4201,i_0_4203,i_0_1035,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217]) ).

cnf(i_0_4369,plain,
    ~ s(s0,s1,s1,s1,s2,s2,p0_1,truck2,truck2,s1,s2,s0),
    inference(scs_inference,[],[i_0_4051,i_0_4045,i_0_4255,i_0_3591,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247]) ).

cnf(i_0_4371,plain,
    s(truck3,truck2,s1,s1,truck3,s1,s0,truck3,p1_2,s1,s0,s2),
    inference(scs_inference,[],[i_0_4143,i_0_4051,i_0_4045,i_0_4255,i_0_3591,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211]) ).

cnf(i_0_4373,plain,
    s(truck2,truck3,s1,s1,s2,s1,truck2,s0,truck1,s1,s2,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4051,i_0_4045,i_0_4255,i_0_3591,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208]) ).

cnf(i_0_4375,plain,
    ~ s(s0,s1,s1,s1,truck2,truck2,s0,truck3,truck2,s1,s2,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_3591,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248]) ).

cnf(i_0_4377,plain,
    ~ s(s0,s1,s1,s1,truck1,truck1,s0,p1_2,truck1,s2,s0,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_3591,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249]) ).

cnf(i_0_4379,plain,
    s(truck3,s0,s1,truck1,truck3,s1,s0,truck3,p1_2,s1,s0,s2),
    inference(scs_inference,[],[i_0_4143,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_3591,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218]) ).

cnf(i_0_4381,plain,
    s(truck3,s0,s1,s1,truck3,truck1,s0,truck3,p1_2,s1,s0,s2),
    inference(scs_inference,[],[i_0_4143,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_3591,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224]) ).

cnf(i_0_4383,plain,
    s(truck3,s0,truck1,s1,truck3,s1,s0,truck3,p1_2,s1,s0,s2),
    inference(scs_inference,[],[i_0_4143,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_3591,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215]) ).

cnf(i_0_4385,plain,
    ~ s(s0,s1,s1,s1,s2,s2,truck3,p0_1,truck2,s1,s1,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_3591,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250]) ).

cnf(i_0_4387,plain,
    ~ s(truck1,s1,s1,s1,s2,s2,s2,truck1,s2,s0,s0,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_3591,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225]) ).

cnf(i_0_4389,plain,
    ~ s(s0,s1,s1,s1,truck1,truck1,s0,truck1,s2,s2,s0,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_3591,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237]) ).

cnf(i_0_4391,plain,
    ~ s(s0,s1,s1,s1,truck3,s2,s0,s2,s2,s1,s0,s2),
    inference(scs_inference,[],[i_0_4143,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239]) ).

cnf(i_0_4393,plain,
    ~ s(s0,s1,s1,s1,s2,truck1,s1,s2,truck1,s2,s0,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240]) ).

cnf(i_0_4395,plain,
    ~ s(s0,truck1,s1,s1,truck3,truck3,p1_2,truck3,s2,s1,s0,s2),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228]) ).

cnf(i_0_4397,plain,
    ~ s(s0,s1,s1,truck1,truck3,truck3,p1_2,truck3,s2,s1,s0,s2),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234]) ).

cnf(i_0_4399,plain,
    ~ s(s0,truck3,truck3,s1,s2,s2,s0,p2_0,p0_1,s1,s0,s1),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230]) ).

cnf(i_0_4401,plain,
    ~ s(s0,s1,truck1,s1,truck3,truck3,p1_2,truck3,s2,s1,s0,s2),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4201,i_0_4203,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231]) ).

cnf(i_0_4403,plain,
    ~ s(s0,truck3,s1,truck3,s2,s2,s0,p2_0,s1,s1,s0,s1),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236]) ).

cnf(i_0_4405,plain,
    ~ s(truck3,s1,s1,s1,truck1,truck1,s0,p1_2,s2,s2,s0,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227]) ).

cnf(i_0_4407,plain,
    ~ s(s0,s1,s1,s1,s2,truck3,s0,s2,s2,s1,s0,s2),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242]) ).

cnf(i_0_4409,plain,
    ~ s(s0,truck3,truck3,s1,s2,s2,s0,p2_0,s1,s1,s0,s1),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233]) ).

cnf(i_0_4411,plain,
    ~ s(s0,truck2,s1,s1,s2,s2,p2_0,s2,s1,s1,s1,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229]) ).

cnf(i_0_4413,plain,
    ~ s(s0,s1,s1,truck2,s2,s2,p2_0,s2,s1,s1,s1,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235]) ).

cnf(i_0_4415,plain,
    ~ s(s0,s1,truck2,s1,s2,s2,p2_0,s2,s1,s1,s1,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232]) ).

cnf(i_0_4417,plain,
    ~ s(s0,s1,s1,s1,truck2,truck2,s0,truck2,truck2,s1,s2,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238]) ).

cnf(i_0_4419,plain,
    ~ s(s0,s1,truck1,s1,truck2,truck2,p2_0,truck2,s2,s1,s2,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3949,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241]) ).

cnf(i_0_4421,plain,
    ~ s(truck2,s1,s1,s1,truck3,truck3,p1_2,truck3,s2,s1,s0,s2),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3949,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226]) ).

cnf(i_0_4423,plain,
    s(truck3,s0,truck3,truck3,s2,truck3,s0,truck3,p0_1,s1,s0,s1),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4123,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3949,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_273,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204]) ).

cnf(i_0_4425,plain,
    s(truck3,s0,s1,s1,truck3,s1,s0,truck3,p1_2,s1,s0,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4051,i_0_4045,i_0_4047,i_0_4123,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3949,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_273,i_0_277,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198]) ).

cnf(i_0_4427,plain,
    s(truck2,s0,s1,truck1,truck2,s1,s0,truck2,truck1,s1,s0,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4037,i_0_4051,i_0_4045,i_0_4047,i_0_4123,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3949,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_273,i_0_277,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199]) ).

cnf(i_0_4429,plain,
    s(s2,truck3,s1,truck2,truck2,truck2,truck2,s0,truck1,s1,s2,s0),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4037,i_0_4051,i_0_4045,i_0_4047,i_0_4123,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3949,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_273,i_0_278,i_0_277,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196]) ).

cnf(i_0_4431,plain,
    s(s2,truck3,s1,s1,truck3,truck3,truck3,s0,truck1,s1,s0,s2),
    inference(scs_inference,[],[i_0_4143,i_0_4033,i_0_4037,i_0_4051,i_0_4045,i_0_4047,i_0_4123,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3949,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_273,i_0_278,i_0_277,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195]) ).

cnf(i_0_4433,plain,
    s(truck1,truck3,s1,s1,s2,s1,s0,p0_1,truck1,s2,s0,s0),
    inference(scs_inference,[],[i_0_3823,i_0_4143,i_0_4033,i_0_4037,i_0_4051,i_0_4045,i_0_4047,i_0_4123,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3949,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_275,i_0_273,i_0_278,i_0_277,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205]) ).

cnf(i_0_4435,plain,
    s(truck1,truck3,s1,s1,s2,s1,p0_1,s0,truck1,s2,s0,s0),
    inference(scs_inference,[],[i_0_3823,i_0_4143,i_0_4033,i_0_4037,i_0_4051,i_0_4045,i_0_4047,i_0_4123,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3949,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_1124,i_0_1035,i_0_3779,i_0_275,i_0_273,i_0_278,i_0_277,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205,i_0_206]) ).

cnf(i_0_4437,plain,
    s(truck1,truck2,s1,s1,truck1,s1,s0,s0,truck1,s1,s0,s0),
    inference(scs_inference,[],[i_0_3823,i_0_4143,i_0_4033,i_0_4037,i_0_4051,i_0_4045,i_0_4047,i_0_4123,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3949,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_4329,i_0_1124,i_0_1035,i_0_3779,i_0_275,i_0_273,i_0_281,i_0_278,i_0_277,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205,i_0_206,i_0_203]) ).

cnf(i_0_4439,plain,
    ~ s(s0,truck1,s1,s1,truck3,truck3,p1_2,s2,s2,s1,s0,s2),
    inference(scs_inference,[],[i_0_3823,i_0_4143,i_0_4033,i_0_4037,i_0_4051,i_0_4045,i_0_4047,i_0_4123,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3949,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_4329,i_0_1124,i_0_1035,i_0_3779,i_0_275,i_0_273,i_0_306,i_0_281,i_0_278,i_0_277,i_0_324,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205,i_0_206,i_0_203,i_0_189]) ).

cnf(i_0_4441,plain,
    ~ s(s0,s1,truck1,s1,truck2,s2,p2_0,s2,s2,s1,s2,s0),
    inference(scs_inference,[],[i_0_3823,i_0_4143,i_0_4033,i_0_4037,i_0_4051,i_0_4045,i_0_4047,i_0_4123,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3949,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_4329,i_0_1124,i_0_1035,i_0_3779,i_0_275,i_0_273,i_0_306,i_0_298,i_0_281,i_0_278,i_0_277,i_0_324,i_0_325,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205,i_0_206,i_0_203,i_0_189,i_0_190]) ).

cnf(i_0_4443,plain,
    s(truck3,s0,truck3,truck3,s2,truck3,s0,truck3,truck1,s1,s0,s1),
    inference(scs_inference,[],[i_0_3823,i_0_4143,i_0_4033,i_0_4037,i_0_4051,i_0_4045,i_0_4047,i_0_4123,i_0_4255,i_0_4343,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3949,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_4329,i_0_1124,i_0_1035,i_0_3779,i_0_275,i_0_273,i_0_306,i_0_298,i_0_353,i_0_281,i_0_278,i_0_277,i_0_344,i_0_324,i_0_325,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205,i_0_206,i_0_203,i_0_189,i_0_190,i_0_194]) ).

cnf(i_0_4445,plain,
    ~ s(s0,truck3,s1,truck3,s2,s2,s1,s2,p2_1,s1,s0,s1),
    inference(scs_inference,[],[i_0_3823,i_0_4143,i_0_4033,i_0_4037,i_0_4051,i_0_4045,i_0_4047,i_0_4123,i_0_4255,i_0_4343,i_0_3849,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3949,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_4329,i_0_1124,i_0_1035,i_0_3779,i_0_275,i_0_273,i_0_288,i_0_306,i_0_298,i_0_353,i_0_281,i_0_278,i_0_277,i_0_344,i_0_324,i_0_325,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205,i_0_206,i_0_203,i_0_189,i_0_190,i_0_194,i_0_186]) ).

cnf(i_0_4448,plain,
    s(truck3,truck3,s1,s1,truck3,truck3,truck3,s0,truck1,s1,s0,s2),
    inference(scs_inference,[],[i_0_3823,i_0_4143,i_0_4033,i_0_4037,i_0_4051,i_0_4045,i_0_4047,i_0_4123,i_0_4255,i_0_4343,i_0_3849,i_0_3591,i_0_3613,i_0_3631,i_0_3666,i_0_3949,i_0_3957,i_0_4125,i_0_4129,i_0_4135,i_0_4165,i_0_4183,i_0_4195,i_0_4201,i_0_4203,i_0_4219,i_0_4329,i_0_1124,i_0_1035,i_0_3779,i_0_275,i_0_273,i_0_288,i_0_306,i_0_298,i_0_353,i_0_281,i_0_278,i_0_277,i_0_344,i_0_324,i_0_325,i_0_244,i_0_251,i_0_246,i_0_243,i_0_213,i_0_222,i_0_245,i_0_216,i_0_210,i_0_223,i_0_214,i_0_217,i_0_247,i_0_211,i_0_208,i_0_248,i_0_249,i_0_218,i_0_224,i_0_215,i_0_250,i_0_225,i_0_237,i_0_239,i_0_240,i_0_228,i_0_234,i_0_230,i_0_231,i_0_236,i_0_227,i_0_242,i_0_233,i_0_229,i_0_235,i_0_232,i_0_238,i_0_241,i_0_226,i_0_204,i_0_198,i_0_199,i_0_196,i_0_195,i_0_205,i_0_206,i_0_203,i_0_189,i_0_190,i_0_194,i_0_186,i_0_207]) ).

cnf(c_0_4465,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X6)
    | ~ s(X1,X2,X3,X4,X5,truck3,X7,X8,X9,X10,X11,X6) ),
    i_0_242 ).

cnf(c_0_4466,plain,
    s(truck3,truck3,s1,s1,truck3,truck3,truck3,s0,truck1,s1,s0,s2),
    i_0_4448 ).

cnf(c_0_4467,axiom,
    ( s(X1,X2,X3,X4,X5,X6,truck3,X7,X8,X9,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,truck3,X7,X8,X9,X10,X12)
    | ~ link(X12,X11) ),
    i_0_195 ).

cnf(c_0_4468,axiom,
    link(s2,s0),
    i_0_277 ).

cnf(c_0_4469,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X5)
    | ~ s(X1,X2,X3,X4,truck3,X6,X7,X8,X9,X10,X11,X5) ),
    i_0_239 ).

cnf(c_0_4470,plain,
    s(truck3,truck3,s1,s1,truck3,s2,truck3,s0,truck1,s1,s0,s2),
    inference(spm,[status(thm)],[c_0_4465,c_0_4466]) ).

cnf(c_0_4471,plain,
    ~ s(s0,truck3,truck3,truck3,s2,s2,p1_2,p2_0,s1,s1,s0,s1),
    i_0_4325 ).

cnf(c_0_4472,axiom,
    ( s(X1,X2,X3,truck3,X4,X5,X6,X7,X8,X9,X10,X11)
    | ~ s(X1,X2,X3,X11,X4,X5,X6,X7,X8,X9,X10,X11) ),
    i_0_216 ).

cnf(c_0_4473,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X9,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X8,truck1,X9,X10,X11) ),
    i_0_249 ).

cnf(c_0_4474,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1)
    | ~ s(truck3,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X1) ),
    i_0_227 ).

cnf(c_0_4475,plain,
    ( s(X1,X2,X3,X4,X5,X6,truck3,X7,X8,X9,X10,s0)
    | ~ s(X1,X2,X3,X4,X5,X6,truck3,X7,X8,X9,X10,s2) ),
    inference(spm,[status(thm)],[c_0_4467,c_0_4468]) ).

cnf(c_0_4476,plain,
    s(truck3,truck3,s1,s1,s2,s2,truck3,s0,truck1,s1,s0,s2),
    inference(spm,[status(thm)],[c_0_4469,c_0_4470]) ).

cnf(c_0_4477,plain,
    ~ s(s0,truck3,truck3,s1,s2,s2,p1_2,p2_0,s1,s1,s0,s1),
    inference(spm,[status(thm)],[c_0_4471,c_0_4472]) ).

cnf(c_0_4478,axiom,
    ( s(X1,X2,truck3,X3,X4,X5,X6,X7,X8,X9,X10,X11)
    | ~ s(X1,X2,X11,X3,X4,X5,X6,X7,X8,X9,X10,X11) ),
    i_0_213 ).

cnf(c_0_4479,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,X13,X9,X10,X11,X12)
    | ~ path(X13,X8) ),
    i_0_205 ).

cnf(c_0_4480,axiom,
    path(s0,p2_0),
    i_0_274 ).

cnf(c_0_4481,axiom,
    link(s0,s1),
    i_0_281 ).

cnf(c_0_4482,plain,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X9,X10,X1)
    | ~ s(truck3,X2,X3,X4,X5,X6,X7,X8,truck1,X9,X10,X1) ),
    inference(spm,[status(thm)],[c_0_4473,c_0_4474]) ).

cnf(c_0_4483,plain,
    s(truck3,truck3,s1,s1,s2,s2,truck3,s0,truck1,s1,s0,s0),
    inference(spm,[status(thm)],[c_0_4475,c_0_4476]) ).

cnf(c_0_4484,plain,
    ~ s(s0,truck3,s1,s1,s2,s2,p1_2,p2_0,s1,s1,s0,s1),
    inference(spm,[status(thm)],[c_0_4477,c_0_4478]) ).

cnf(c_0_4485,plain,
    ( s(X1,X2,X3,X4,X5,X6,X7,p2_0,X8,X9,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,X7,s0,X8,X9,X10,X11) ),
    inference(spm,[status(thm)],[c_0_4479,c_0_4480]) ).

cnf(c_0_4486,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X12)
    | ~ s(X1,X2,X3,X4,X5,X6,X13,X8,X9,X10,X11,X12)
    | ~ path(X13,X7) ),
    i_0_206 ).

cnf(c_0_4487,axiom,
    path(s1,p1_2),
    i_0_272 ).

cnf(c_0_4488,plain,
    ( s(X1,X2,X3,X4,X5,X6,truck3,X7,X8,X9,X10,s1)
    | ~ s(X1,X2,X3,X4,X5,X6,truck3,X7,X8,X9,X10,s0) ),
    inference(spm,[status(thm)],[c_0_4467,c_0_4481]) ).

cnf(c_0_4489,plain,
    s(s0,truck3,s1,s1,s2,s2,truck3,s0,s1,s1,s0,s0),
    inference(spm,[status(thm)],[c_0_4482,c_0_4483]) ).

cnf(c_0_4490,plain,
    ~ s(s0,truck3,s1,s1,s2,s2,p1_2,s0,s1,s1,s0,s1),
    inference(spm,[status(thm)],[c_0_4484,c_0_4485]) ).

cnf(c_0_4491,plain,
    ( s(X1,X2,X3,X4,X5,X6,p1_2,X7,X8,X9,X10,X11)
    | ~ s(X1,X2,X3,X4,X5,X6,s1,X7,X8,X9,X10,X11) ),
    inference(spm,[status(thm)],[c_0_4486,c_0_4487]) ).

cnf(c_0_4492,axiom,
    ( s(X1,X2,X3,X4,X5,X6,X7,X8,X9,X10,X11,X7)
    | ~ s(X1,X2,X3,X4,X5,X6,truck3,X8,X9,X10,X11,X7) ),
    i_0_245 ).

cnf(c_0_4493,plain,
    s(s0,truck3,s1,s1,s2,s2,truck3,s0,s1,s1,s0,s1),
    inference(spm,[status(thm)],[c_0_4488,c_0_4489]) ).

cnf(c_0_4494,plain,
    ~ s(s0,truck3,s1,s1,s2,s2,s1,s0,s1,s1,s0,s1),
    inference(spm,[status(thm)],[c_0_4490,c_0_4491]) ).

cnf(c_0_4495,plain,
    $false,
    inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_4492,c_0_4493]),c_0_4494]),
    [proof] ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem    : PLA031-1.007 : TPTP v9.2.1. Released v3.5.0.
% 0.00/0.12  % Command    : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33  % Computer : n010.cluster.edu
% 0.15/0.33  % Model    : x86_64 x86_64
% 0.15/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33  % Memory   : 8042.1875MB
% 0.15/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33  % CPULimit   : 300
% 0.15/0.33  % WCLimit    : 300
% 0.15/0.33  % DateTime   : Tue May  5 01:27:06 EDT 2026
% 0.15/0.33  % CPUTime    : 
% 0.15/0.34  % start to proof: theBenchmark
% 242.22/127.67  % Version  : CSE_E---1.7
% 242.22/127.67  % Problem  : theBenchmark.p
% 242.22/127.67  % SZS status Unsatisfiable for theBenchmark.p
% 242.22/127.67  % SZS output start CNFRefutation
% See solution above
% 253.22/138.69  % Total time : 126.147s
%------------------------------------------------------------------------------