The cat chases the tiger. The cat eats the cow. The cat is blue. The cat is nice. The cat is red. The cat is round. The cat is young. The cat likes the tiger. The cow chases the tiger. The cow is nice. The cow likes the cat. The tiger chases the cat. The tiger eats the cat. The tiger eats the cow. The tiger is nice. The tiger likes the cat. If something is round then it likes the cat. If something likes the cow and it is red then the cow is nice. If something is round then it likes the tiger. If something likes the cat and it is young then it eats the cat. If something chases the tiger then it likes the cat. If something chases the cat and it is young then it is blue. If something is young and it likes the tiger then it is nice. If something is nice and red then it chases the cow.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If something is round then it likes the cat.
((("something" "is" "round" "+")) -> ("something" "likes" "cat" "+"))
If something likes the cow and it is red then the cow is nice.
((("something" "likes" "cow" "+") ("something" "is" "red" "+")) -> ("cow" "is" "nice" "+"))
If something is round then it likes the tiger.
((("something" "is" "round" "+")) -> ("something" "likes" "tiger" "+"))
If something likes the cat and it is young then it eats the cat.
((("something" "likes" "cat" "+") ("something" "is" "young" "+")) -> ("something" "eats" "cat" "+"))
If something chases the tiger then it likes the cat.
((("something" "chases" "tiger" "+")) -> ("something" "likes" "cat" "+"))
If something chases the cat and it is young then it is blue.
((("something" "chases" "cat" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is young and it likes the tiger then it is nice.
((("something" "is" "young" "+") ("something" "likes" "tiger" "+")) -> ("something" "is" "nice" "+"))
If something is nice and red then it chases the cow.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "chases" "cow" "+"))
The cow is nice.
True
1
proof
[(triple10)]
("cow" "is" "nice" "+")
triple10
The tiger is not nice.
False
1
inv-proof
[(triple15)]
("tiger" "is" "nice" "-")
triple15
The cat chases the cow.
True
3
proof
[(((triple4 triple5) -> rule8) OR ((((triple7 triple8) -> rule7) triple5) -> rule8) OR ((((triple7 ((triple6) -> rule3)) -> rule7) triple5) -> rule8))]
("cat" "chases" "cow" "+")
((triple4 triple5) -> (rule8 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
((((triple7 triple8) -> (rule7 % int2)) triple5) -> (rule8 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule7 % int2)) triple5) -> (rule8 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The cat does not like the cat.
False
2
inv-proof
[(((triple1) -> rule5) OR ((triple6) -> rule1))]
("cat" "likes" "cat" "-")
((triple1) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
((triple6) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat eats the cat.
True
4
proof
[(((((triple1) -> rule5) triple7) -> rule4) OR ((((triple6) -> rule1) triple7) -> rule4))]
("cat" "eats" "cat" "+")
((((triple1) -> (rule5 % int2)) triple7) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((triple6) -> (rule1 % int2)) triple7) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat does not eat the cat.
False
4
inv-proof
[(((((triple1) -> rule5) triple7) -> rule4) OR ((((triple6) -> rule1) triple7) -> rule4))]
("cat" "eats" "cat" "-")
((((triple1) -> (rule5 % int2)) triple7) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((triple6) -> (rule1 % int2)) triple7) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cow does not eat the cat.
Unknown
inv-rconc
[@1: The cow eats the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "eats" "cat" "-")
The tiger likes the tiger.
Unknown
rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "likes" "tiger" "+")
The cow does not like the tiger.
Unknown
inv-rconc
[@1: The cow likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "likes" "tiger" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
The cow does not chase the cat.
Unknown
inv-random
[@0: The cow chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cat" "-")
The cow eats the tiger.
Unknown
random
[@0: The cow eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "tiger" "+")
@0: The cat chases the tiger.[(triple1)] The cat eats the cow.[(triple2)] The cat is blue.[(triple3)] The cat is nice.[(triple4 OR ((triple7 triple8) -> rule7) OR ((triple7 ((triple6) -> rule3)) -> rule7))] The cat is red.[(triple5)] The cat is round.[(triple6)] The cat is young.[(triple7)] The cat likes the tiger.[(triple8 OR ((triple6) -> rule3))] The cow chases the tiger.[(triple9)] The cow is nice.[(triple10)] The cow likes the cat.[(triple11 OR ((triple9) -> rule5))] The tiger chases the cat.[(triple12)] The tiger eats the cat.[(triple13)] The tiger eats the cow.[(triple14)] The tiger is nice.[(triple15)] The tiger likes the cat.[(triple16)] @1: The cat chases the cow.[(((triple4 triple5) -> rule8) OR ((((triple7 triple8) -> rule7) triple5) -> rule8) OR ((((triple7 ((triple6) -> rule3)) -> rule7) triple5) -> rule8))] The cat likes the cat.[(((triple1) -> rule5) OR ((triple6) -> rule1))] @2: The cat eats the cat.[(((((triple1) -> rule5) triple7) -> rule4) OR ((((triple6) -> rule1) triple7) -> rule4))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cat eats the cow.
("cat" "eats" "cow" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is nice.
("cat" "is" "nice" "+")
triple4
((triple7 triple8) -> (rule7 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
((triple7 ((triple6) -> (rule3 % int2))) -> (rule7 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int2
The cat is red.
("cat" "is" "red" "+")
triple5
The cat is round.
("cat" "is" "round" "+")
triple6
The cat is young.
("cat" "is" "young" "+")
triple7
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple8
((triple6) -> (rule3 % int1))
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple9
The cow is nice.
("cow" "is" "nice" "+")
triple10
The cow likes the cat.
("cow" "likes" "cat" "+")
triple11
((triple9) -> (rule5 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple12
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple13
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple14
The tiger is nice.
("tiger" "is" "nice" "+")
triple15
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple16
The cat chases the cow.
("cat" "chases" "cow" "+")
((triple4 triple5) -> (rule8 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
((((triple7 triple8) -> (rule7 % int2)) triple5) -> (rule8 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule7 % int2)) triple5) -> (rule8 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat likes the tiger.
("cat" "likes" "tiger" "+")
int3
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple1) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
((triple6) -> (rule1 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
((((triple1) -> (rule5 % int2)) triple7) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((triple6) -> (rule1 % int2)) triple7) -> (rule4 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2