@prefix skolem: <https://eyereasoner.github.io/.well-known/genid/8b98b360-9a70-4845-b52c-c675af60ad01#>.
@prefix r: <http://www.w3.org/2000/10/swap/reason#>.
@prefix log: <http://www.w3.org/2000/10/swap/log#>.
@prefix : <http://eulersharp.sourceforge.net/2005/11swap/zebra#>.
@prefix n3: <http://www.w3.org/2004/06/rei#>.
@prefix var: <http://www.w3.org/2000/10/swap/var#>.
@prefix list: <http://www.w3.org/2000/10/swap/list#>.

skolem:proof a r:Proof, r:Conjunction;
    r:component skolem:lemma1;
    r:gives [ log:graph (
        [ log:triple (:german :eats :fish)]
    )].

skolem:lemma1 a r:Inference;
    r:gives [ log:graph (
        [ log:triple (:german :eats :fish)]
    )];
    r:evidence (
        skolem:lemma2
    );
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#german"]];
    r:rule [ a r:Fact; r:gives [ log:graph ([ log:triple ([ log:graph (
        [ log:triple (var:x_0 :eats :fish)]
    )] log:implies [ log:graph (
        [ log:triple (var:x_0 :eats :fish)]
    )])])]].

skolem:lemma2 a r:Inference;
    r:gives [ log:graph (
        [ log:triple (:german :eats :fish)]
    )];
    r:evidence (
        [ a r:Fact; r:gives [ log:graph ([ log:triple (((:yellow :norwegian :cats :water :dunhill) (:blue :dane :horse :tea :blends) (:red :brit :birds :milk :pallmall) (:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters)) log:equalTo ((:yellow :norwegian :cats :water :dunhill) (:blue :dane :horse :tea :blends) (:red :brit :birds :milk :pallmall) (:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters)))])]]
        [ a r:Fact; r:gives [ log:graph ([ log:triple (((:yellow :norwegian :cats :water :dunhill) (:blue :dane :horse :tea :blends) (:red :brit :birds :milk :pallmall) (:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters)) :pair ((:blue :dane :horse :tea :blends) (:yellow :norwegian :cats :water :dunhill)))])]]
        [ a r:Fact; r:gives [ log:graph ([ log:triple (((:yellow :norwegian :cats :water :dunhill) (:blue :dane :horse :tea :blends) (:red :brit :birds :milk :pallmall) (:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters)) :pair ((:blue :dane :horse :tea :blends) (:yellow :norwegian :cats :water :dunhill)))])]]
        [ a r:Fact; r:gives [ log:graph ([ log:triple (((:yellow :norwegian :cats :water :dunhill) (:blue :dane :horse :tea :blends) (:red :brit :birds :milk :pallmall) (:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters)) :sublist ((:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters)))])]]
        [ a r:Fact; r:gives [ log:graph ([ log:triple (((:yellow :norwegian :cats :water :dunhill) (:blue :dane :horse :tea :blends) (:red :brit :birds :milk :pallmall) (:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters)) :pair ((:blue :dane :horse :tea :blends) (:yellow :norwegian :cats :water :dunhill)))])]]
        [ a r:Fact; r:gives [ log:graph ([ log:triple (((:yellow :norwegian :cats :water :dunhill) (:blue :dane :horse :tea :blends) (:red :brit :birds :milk :pallmall) (:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters)) list:member (:red :brit :birds :milk :pallmall))])]]
        [ a r:Fact; r:gives [ log:graph ([ log:triple (((:yellow :norwegian :cats :water :dunhill) (:blue :dane :horse :tea :blends) (:red :brit :birds :milk :pallmall) (:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters)) list:member (:white :swede :dogs :beer :bluemasters))])]]
        [ a r:Fact; r:gives [ log:graph ([ log:triple (((:yellow :norwegian :cats :water :dunhill) (:blue :dane :horse :tea :blends) (:red :brit :birds :milk :pallmall) (:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters)) list:member (:blue :dane :horse :tea :blends))])]]
        [ a r:Fact; r:gives [ log:graph ([ log:triple (((:yellow :norwegian :cats :water :dunhill) (:blue :dane :horse :tea :blends) (:red :brit :birds :milk :pallmall) (:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters)) list:member (:red :brit :birds :milk :pallmall))])]]
        [ a r:Fact; r:gives [ log:graph ([ log:triple (((:yellow :norwegian :cats :water :dunhill) (:blue :dane :horse :tea :blends) (:red :brit :birds :milk :pallmall) (:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters)) list:member (:yellow :norwegian :cats :water :dunhill))])]]
        [ a r:Fact; r:gives [ log:graph ([ log:triple (((:yellow :norwegian :cats :water :dunhill) (:blue :dane :horse :tea :blends) (:red :brit :birds :milk :pallmall) (:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters)) list:member (:white :swede :dogs :beer :bluemasters))])]]
        [ a r:Fact; r:gives [ log:graph ([ log:triple (((:yellow :norwegian :cats :water :dunhill) (:blue :dane :horse :tea :blends) (:red :brit :birds :milk :pallmall) (:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters)) list:member (:green :german :fish :coffee :prince))])]]
        [ a r:Fact; r:gives [ log:graph ([ log:triple (((:yellow :norwegian :cats :water :dunhill) (:blue :dane :horse :tea :blends) (:red :brit :birds :milk :pallmall) (:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters)) list:member (:green :german :fish :coffee :prince))])]]
    );
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_0"]; r:boundTo ((:yellow :norwegian :cats :water :dunhill) (:blue :dane :horse :tea :blends) (:red :brit :birds :milk :pallmall) (:green :german :fish :coffee :prince) (:white :swede :dogs :beer :bluemasters))];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_1"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#yellow"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_2"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#cats"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_3"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#water"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_4"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#dunhill"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_5"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#dane"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_6"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#horse"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_7"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#tea"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_8"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#blends"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_9"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#red"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_10"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#brit"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_11"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#birds"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_12"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#pallmall"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_13"]; r:boundTo (:green :german :fish :coffee :prince)];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_14"]; r:boundTo (:white :swede :dogs :beer :bluemasters)];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_15"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#blue"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_16"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#dane"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_17"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#horse"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_18"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#tea"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_19"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#yellow"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_20"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#norwegian"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_21"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#water"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_22"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#dunhill"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_23"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#blue"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_24"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#dane"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_25"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#tea"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_26"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#blends"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_27"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#yellow"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_28"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#norwegian"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_29"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#cats"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_30"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#water"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_31"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#german"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_32"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#fish"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_33"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#prince"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_34"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#swede"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_35"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#dogs"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_36"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#beer"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_37"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#bluemasters"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_38"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#blue"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_39"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#dane"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_40"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#horse"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_41"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#tea"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_42"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#yellow"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_43"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#norwegian"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_44"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#cats"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_45"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#dunhill"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_46"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#birds"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_47"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#milk"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_48"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#pallmall"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_49"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#white"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_50"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#beer"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_51"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#bluemasters"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_52"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#blue"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_53"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#horse"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_54"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#blends"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_55"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#red"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_56"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#brit"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_57"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#milk"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_58"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#norwegian"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_59"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#cats"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_60"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#water"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_61"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#white"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_62"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#swede"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_63"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#dogs"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_64"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#green"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_65"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#fish"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_66"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#coffee"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_67"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#green"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_68"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#german"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_69"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#coffee"]];
    r:binding [ r:variable [ n3:uri "http://www.w3.org/2000/10/swap/var#x_70"]; r:boundTo [ n3:uri "http://eulersharp.sourceforge.net/2005/11swap/zebra#prince"]];
    r:rule [ a r:Fact; r:gives [ log:graph ([ log:triple ([ log:graph (
        [ log:triple (var:x_0 log:equalTo ((var:x_1 :norwegian var:x_2 var:x_3 var:x_4) (:blue var:x_5 var:x_6 var:x_7 var:x_8) (var:x_9 var:x_10 var:x_11 :milk var:x_12) var:x_13 var:x_14))]
        [ log:triple (var:x_0 :pair ((var:x_15 var:x_16 var:x_17 var:x_18 :blends) (var:x_19 var:x_20 :cats var:x_21 var:x_22)))]
        [ log:triple (var:x_0 :pair ((var:x_23 var:x_24 :horse var:x_25 var:x_26) (var:x_27 var:x_28 var:x_29 var:x_30 :dunhill)))]
        [ log:triple (var:x_0 :sublist ((:green var:x_31 var:x_32 :coffee var:x_33) (:white var:x_34 var:x_35 var:x_36 var:x_37)))]
        [ log:triple (var:x_0 :pair ((var:x_38 var:x_39 var:x_40 var:x_41 :blends) (var:x_42 var:x_43 var:x_44 :water var:x_45)))]
        [ log:triple (var:x_0 list:member (:red :brit var:x_46 var:x_47 var:x_48))]
        [ log:triple (var:x_0 list:member (var:x_49 :swede :dogs var:x_50 var:x_51))]
        [ log:triple (var:x_0 list:member (var:x_52 :dane var:x_53 :tea var:x_54))]
        [ log:triple (var:x_0 list:member (var:x_55 var:x_56 :birds var:x_57 :pallmall))]
        [ log:triple (var:x_0 list:member (:yellow var:x_58 var:x_59 var:x_60 :dunhill))]
        [ log:triple (var:x_0 list:member (var:x_61 var:x_62 var:x_63 :beer :bluemasters))]
        [ log:triple (var:x_0 list:member (var:x_64 :german var:x_65 var:x_66 :prince))]
        [ log:triple (var:x_0 list:member (var:x_67 var:x_68 :fish var:x_69 var:x_70))]
    )] log:implies [ log:graph (
        [ log:triple (var:x_68 :eats :fish)]
    )])])]].

