The cat is blue. The cat is green. The cat is kind. The cat is nice. The cat is red. The cat likes the cow. The cat needs the cow. The cat sees the cow. The cow is blue. The cow is green. The cow is nice. The cow is red. The cow likes the cat. The cow needs the cat. The cow sees the cat. If the cow is green then the cow needs the cat. If someone sees the cat and they see the cow then they need the cat. If the cat is blue and the cat is red then the cat likes the cow. If someone likes the cat then the cat is kind. If someone likes the cow then they like the cat. If the cow is blue then the cow needs the cat. If someone likes the cat then they see the cat. If someone is nice and they see the cat then they are red.
The cat is blue.
("cat" "is" "blue" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is red.
("cat" "is" "red" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
If the cow is green then the cow needs the cat.
((("cow" "is" "green" "+")) -> ("cow" "needs" "cat" "+"))
If someone sees the cat and they see the cow then they need the cat.
((("someone" "sees" "cat" "+") ("someone" "sees" "cow" "+")) -> ("someone" "needs" "cat" "+"))
If the cat is blue and the cat is red then the cat likes the cow.
((("cat" "is" "blue" "+") ("cat" "is" "red" "+")) -> ("cat" "likes" "cow" "+"))
If someone likes the cat then the cat is kind.
((("someone" "likes" "cat" "+")) -> ("cat" "is" "kind" "+"))
If someone likes the cow then they like the cat.
((("someone" "likes" "cow" "+")) -> ("someone" "likes" "cat" "+"))
If the cow is blue then the cow needs the cat.
((("cow" "is" "blue" "+")) -> ("cow" "needs" "cat" "+"))
If someone likes the cat then they see the cat.
((("someone" "likes" "cat" "+")) -> ("someone" "sees" "cat" "+"))
If someone is nice and they see the cat then they are red.
((("someone" "is" "nice" "+") ("someone" "sees" "cat" "+")) -> ("someone" "is" "red" "+"))
The cow is blue.
True
1
proof
[(triple9)]
("cow" "is" "blue" "+")
triple9
The cow does not see the cat.
False
1
inv-proof
[(triple15 OR ((triple13) -> rule7))]
("cow" "sees" "cat" "-")
triple15
((triple13) -> (rule7 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cat likes the cat.
True
2
proof
[(((triple6) -> rule5) OR ((((triple1 triple5) -> rule3)) -> rule5))]
("cat" "likes" "cat" "+")
((triple6) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
((((triple1 triple5) -> (rule3 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cat does not like the cat.
False
2
inv-proof
[(((triple6) -> rule5) OR ((((triple1 triple5) -> rule3)) -> rule5))]
("cat" "likes" "cat" "-")
((triple6) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
((((triple1 triple5) -> (rule3 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cat sees the cat.
True
3
proof
[(((((triple6) -> rule5)) -> rule7) OR ((((((triple1 triple5) -> rule3)) -> rule5)) -> rule7))]
("cat" "sees" "cat" "+")
((((triple6) -> (rule5 % int2))) -> (rule7 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((((triple1 triple5) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The cat does not see the cat.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule7) OR ((((((triple1 triple5) -> rule3)) -> rule5)) -> rule7))]
("cat" "sees" "cat" "-")
((((triple6) -> (rule5 % int2))) -> (rule7 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((((triple1 triple5) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The cat needs the cat.
True
5
proof
[(((((((triple6) -> rule5)) -> rule7) triple8) -> rule2) OR ((((((((triple1 triple5) -> rule3)) -> rule5)) -> rule7) triple8) -> rule2))]
("cat" "needs" "cat" "+")
((((((triple6) -> (rule5 % int3))) -> (rule7 % int2)) triple8) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
((((((((triple1 triple5) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule7 % int2)) triple8) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
The cat likes the cow.
("cat" "likes" "cow" "+")
int4
The cat does not need the cat.
False
5
inv-proof
[(((((((triple6) -> rule5)) -> rule7) triple8) -> rule2) OR ((((((((triple1 triple5) -> rule3)) -> rule5)) -> rule7) triple8) -> rule2))]
("cat" "needs" "cat" "-")
((((((triple6) -> (rule5 % int3))) -> (rule7 % int2)) triple8) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
((((((((triple1 triple5) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule7 % int2)) triple8) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
The cat likes the cow.
("cat" "likes" "cow" "+")
int4
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
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 need the cow.
Unknown
inv-random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cat is blue.[(triple1)] The cat is green.[(triple2)] The cat is kind.[(triple3 OR ((triple13) -> rule4) OR ((((triple6) -> rule5)) -> rule4) OR ((((((triple1 triple5) -> rule3)) -> rule5)) -> rule4))] The cat is nice.[(triple4)] The cat is red.[(triple5 OR ((triple4 ((((triple6) -> rule5)) -> rule7)) -> rule8))] The cat likes the cow.[(triple6 OR ((triple1 triple5) -> rule3))] The cat needs the cow.[(triple7)] The cat sees the cow.[(triple8)] The cow is blue.[(triple9)] The cow is green.[(triple10)] The cow is nice.[(triple11)] The cow is red.[(triple12 OR ((triple11 triple15) -> rule8) OR ((triple11 ((triple13) -> rule7)) -> rule8))] The cow likes the cat.[(triple13)] The cow needs the cat.[(triple14 OR ((triple10) -> rule1) OR ((triple9) -> rule6))] The cow sees the cat.[(triple15 OR ((triple13) -> rule7))] @1: The cat likes the cat.[(((triple6) -> rule5) OR ((((triple1 triple5) -> rule3)) -> rule5))] @2: The cat sees the cat.[(((((triple6) -> rule5)) -> rule7) OR ((((((triple1 triple5) -> rule3)) -> rule5)) -> rule7))] @3: The cat needs the cat.[(((((((triple6) -> rule5)) -> rule7) triple8) -> rule2) OR ((((((((triple1 triple5) -> rule3)) -> rule5)) -> rule7) triple8) -> rule2))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
((triple13) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((((triple1 triple5) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The cat is nice.
("cat" "is" "nice" "+")
triple4
The cat is red.
("cat" "is" "red" "+")
triple5
((triple4 ((((triple6) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
The cat likes the cow.
("cat" "likes" "cow" "+")
triple6
((triple1 triple5) -> (rule3 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
triple7
The cat sees the cow.
("cat" "sees" "cow" "+")
triple8
The cow is blue.
("cow" "is" "blue" "+")
triple9
The cow is green.
("cow" "is" "green" "+")
triple10
The cow is nice.
("cow" "is" "nice" "+")
triple11
The cow is red.
("cow" "is" "red" "+")
triple12
((triple11 triple15) -> (rule8 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
((triple11 ((triple13) -> (rule7 % int2))) -> (rule8 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
int2
The cow likes the cat.
("cow" "likes" "cat" "+")
triple13
The cow needs the cat.
("cow" "needs" "cat" "+")
triple14
((triple10) -> (rule1 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
((triple9) -> (rule6 % int1))
The cow needs the cat.
("cow" "needs" "cat" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
triple15
((triple13) -> (rule7 % int1))
The cow sees the cat.
("cow" "sees" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple6) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
((((triple1 triple5) -> (rule3 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
((((triple6) -> (rule5 % int2))) -> (rule7 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
((((((triple1 triple5) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The cat needs the cat.
("cat" "needs" "cat" "+")
((((((triple6) -> (rule5 % int3))) -> (rule7 % int2)) triple8) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
((((((((triple1 triple5) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule7 % int2)) triple8) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
The cat likes the cow.
("cat" "likes" "cow" "+")
int4