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