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