The cat eats the lion. The dog eats the lion. The dog is green. The dog needs the lion. The dog sees the squirrel. The lion is blue. The lion is nice. The squirrel is blue. The squirrel is green. The squirrel needs the cat. If something needs the dog and the dog sees the squirrel then it sees the squirrel. If something is green and it eats the dog then it eats the squirrel. If something is green then it eats the dog. If the squirrel sees the lion then the lion sees the dog. If something eats the squirrel then it is young. If something is young and it eats the lion then the lion is green. If the lion needs the dog and the dog needs the squirrel then the lion needs the cat. If something needs the lion and the lion eats the cat then it eats the lion. If something eats the lion then it sees the cat.
The cat eats the lion.
("cat" "eats" "lion" "+")
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is green.
("dog" "is" "green" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is nice.
("lion" "is" "nice" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
If something needs the dog and the dog sees the squirrel then it sees the squirrel.
((("something" "needs" "dog" "+") ("dog" "sees" "squirrel" "+")) -> ("something" "sees" "squirrel" "+"))
If something is green and it eats the dog then it eats the squirrel.
((("something" "is" "green" "+") ("something" "eats" "dog" "+")) -> ("something" "eats" "squirrel" "+"))
If something is green then it eats the dog.
((("something" "is" "green" "+")) -> ("something" "eats" "dog" "+"))
If the squirrel sees the lion then the lion sees the dog.
((("squirrel" "sees" "lion" "+")) -> ("lion" "sees" "dog" "+"))
If something eats the squirrel then it is young.
((("something" "eats" "squirrel" "+")) -> ("something" "is" "young" "+"))
If something is young and it eats the lion then the lion is green.
((("something" "is" "young" "+") ("something" "eats" "lion" "+")) -> ("lion" "is" "green" "+"))
If the lion needs the dog and the dog needs the squirrel then the lion needs the cat.
((("lion" "needs" "dog" "+") ("dog" "needs" "squirrel" "+")) -> ("lion" "needs" "cat" "+"))
If something needs the lion and the lion eats the cat then it eats the lion.
((("something" "needs" "lion" "+") ("lion" "eats" "cat" "+")) -> ("something" "eats" "lion" "+"))
If something eats the lion then it sees the cat.
((("something" "eats" "lion" "+")) -> ("something" "sees" "cat" "+"))
The dog eats the lion.
True
1
proof
[(triple2)]
("dog" "eats" "lion" "+")
triple2
The squirrel is not green.
False
1
inv-proof
[(triple9)]
("squirrel" "is" "green" "-")
triple9
The dog sees the cat.
True
2
proof
[(((triple2) -> rule9))]
("dog" "sees" "cat" "+")
((triple2) -> (rule9 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The squirrel does not eat the dog.
False
2
inv-proof
[(((triple9) -> rule3))]
("squirrel" "eats" "dog" "-")
((triple9) -> (rule3 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The dog eats the squirrel.
True
4
proof
[(((triple3 ((triple3) -> rule3)) -> rule2))]
("dog" "eats" "squirrel" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The squirrel does not eat the squirrel.
False
4
inv-proof
[(((triple9 ((triple9) -> rule3)) -> rule2))]
("squirrel" "eats" "squirrel" "-")
((triple9 ((triple9) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int2
The squirrel is young.
True
5
proof
[(((((triple9 ((triple9) -> rule3)) -> rule2)) -> rule5))]
("squirrel" "is" "young" "+")
((((triple9 ((triple9) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int3
The dog is not young.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule3)) -> rule2)) -> rule5))]
("dog" "is" "young" "-")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
int3
The lion is green.
True
7
proof
[(((((((triple3 ((triple3) -> rule3)) -> rule2)) -> rule5) triple2) -> rule6))]
("lion" "is" "green" "+")
((((((triple3 ((triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) triple2) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int3
The dog eats the dog.
("dog" "eats" "dog" "+")
int4
The lion is not green.
False
7
inv-proof
[(((((((triple3 ((triple3) -> rule3)) -> rule2)) -> rule5) triple2) -> rule6))]
("lion" "is" "green" "-")
((((((triple3 ((triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) triple2) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int3
The dog eats the dog.
("dog" "eats" "dog" "+")
int4
The lion eats the dog.
True
8
proof
[(((((((((triple3 ((triple3) -> rule3)) -> rule2)) -> rule5) triple2) -> rule6)) -> rule3))]
("lion" "eats" "dog" "+")
((((((((triple3 ((triple3) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule5 % int3)) triple2) -> (rule6 % int2))) -> (rule3 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int4
The dog eats the dog.
("dog" "eats" "dog" "+")
int5
The lion does not eat the dog.
False
8
inv-proof
[(((((((((triple3 ((triple3) -> rule3)) -> rule2)) -> rule5) triple2) -> rule6)) -> rule3))]
("lion" "eats" "dog" "-")
((((((((triple3 ((triple3) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule5 % int3)) triple2) -> (rule6 % int2))) -> (rule3 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int4
The dog eats the dog.
("dog" "eats" "dog" "+")
int5
The lion does not see the dog.
Unknown
inv-rconc
[@1: The lion sees the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "sees" "dog" "-")
The squirrel sees the squirrel.
Unknown
rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel does not see the cat.
Unknown
inv-rconc
[@2: The squirrel sees the cat.[CWA. Example of deepest failure = (rule9 <- rule8 <- FAIL)]]
("squirrel" "sees" "cat" "-")
The lion sees the squirrel.
Unknown
rconc
[@1: The lion sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "squirrel" "+")
The cat does not eat the dog.
Unknown
inv-rconc
[@1: The cat eats the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "eats" "dog" "-")
The lion needs the cat.
Unknown
rconc
[@1: The lion needs the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "needs" "cat" "+")
The cat does not see the lion.
Unknown
inv-random
[@0: The cat sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "lion" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The cat does not need the dog.
Unknown
inv-random
[@0: The cat needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "dog" "-")
The dog needs the cat.
Unknown
random
[@0: The dog needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cat" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
@0: The cat eats the lion.[(triple1)] The dog eats the lion.[(triple2)] The dog is green.[(triple3)] The dog needs the lion.[(triple4)] The dog sees the squirrel.[(triple5)] The lion is blue.[(triple6)] The lion is nice.[(triple7)] The squirrel is blue.[(triple8)] The squirrel is green.[(triple9)] The squirrel needs the cat.[(triple10)] @1: The cat sees the cat.[(((triple1) -> rule9))] The dog eats the dog.[(((triple3) -> rule3))] The dog sees the cat.[(((triple2) -> rule9))] The squirrel eats the dog.[(((triple9) -> rule3))] @2: The dog eats the squirrel.[(((triple3 ((triple3) -> rule3)) -> rule2))] The squirrel eats the squirrel.[(((triple9 ((triple9) -> rule3)) -> rule2))] @3: The dog is young.[(((((triple3 ((triple3) -> rule3)) -> rule2)) -> rule5))] The squirrel is young.[(((((triple9 ((triple9) -> rule3)) -> rule2)) -> rule5))] @4: The lion is green.[(((((((triple3 ((triple3) -> rule3)) -> rule2)) -> rule5) triple2) -> rule6))] @5: The lion eats the dog.[(((((((((triple3 ((triple3) -> rule3)) -> rule2)) -> rule5) triple2) -> rule6)) -> rule3))] @6: The lion eats the squirrel.[(((((((((triple3 ((triple3) -> rule3)) -> rule2)) -> rule5) triple2) -> rule6) ((((((((triple3 ((triple3) -> rule3)) -> rule2)) -> rule5) triple2) -> rule6)) -> rule3)) -> rule2))] @7: The lion is young.[(((((((((((triple3 ((triple3) -> rule3)) -> rule2)) -> rule5) triple2) -> rule6) ((((((((triple3 ((triple3) -> rule3)) -> rule2)) -> rule5) triple2) -> rule6)) -> rule3)) -> rule2)) -> rule5))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The dog eats the lion.
("dog" "eats" "lion" "+")
triple2
The dog is green.
("dog" "is" "green" "+")
triple3
The dog needs the lion.
("dog" "needs" "lion" "+")
triple4
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple5
The lion is blue.
("lion" "is" "blue" "+")
triple6
The lion is nice.
("lion" "is" "nice" "+")
triple7
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple8
The squirrel is green.
("squirrel" "is" "green" "+")
triple9
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple10
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple1) -> (rule9 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
((triple3) -> (rule3 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
((triple2) -> (rule9 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
((triple9) -> (rule3 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The dog eats the dog.
("dog" "eats" "dog" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((triple9 ((triple9) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int2
The dog is young.
("dog" "is" "young" "+")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
int3
The squirrel is young.
("squirrel" "is" "young" "+")
((((triple9 ((triple9) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int3
The lion is green.
("lion" "is" "green" "+")
((((((triple3 ((triple3) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) triple2) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int3
The dog eats the dog.
("dog" "eats" "dog" "+")
int4
The lion eats the dog.
("lion" "eats" "dog" "+")
((((((((triple3 ((triple3) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule5 % int3)) triple2) -> (rule6 % int2))) -> (rule3 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int4
The dog eats the dog.
("dog" "eats" "dog" "+")
int5
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
((((((((triple3 ((triple3) -> (rule3 % int6))) -> (rule2 % int5))) -> (rule5 % int4)) triple2) -> (rule6 % int3)) ((((((((triple3 ((triple3) -> (rule3 % int6))) -> (rule2 % int5))) -> (rule5 % int4)) triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The lion eats the dog.
("lion" "eats" "dog" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The dog is young.
("dog" "is" "young" "+")
int4
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int5
The dog eats the dog.
("dog" "eats" "dog" "+")
int6
The lion is young.
("lion" "is" "young" "+")
((((((((((triple3 ((triple3) -> (rule3 % int7))) -> (rule2 % int6))) -> (rule5 % int5)) triple2) -> (rule6 % int4)) ((((((((triple3 ((triple3) -> (rule3 % int7))) -> (rule2 % int6))) -> (rule5 % int5)) triple2) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
The lion eats the dog.
("lion" "eats" "dog" "+")
int3
The lion is green.
("lion" "is" "green" "+")
int4
The dog is young.
("dog" "is" "young" "+")
int5
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int6
The dog eats the dog.
("dog" "eats" "dog" "+")
int7