The cat is blue. The cat is green. The cat is red. The cat is round. The cat likes the squirrel. The cat needs the squirrel. The cat sees the squirrel. The squirrel is red. The squirrel is round. The squirrel likes the cat. The squirrel needs the cat. The squirrel sees the cat. If something likes the cat then the cat likes the squirrel. If something is cold and it needs the squirrel then it needs the cat. If something is green then it sees the cat. All round things are cold. If the squirrel needs the cat then the squirrel likes the cat. If something is blue and it needs the squirrel then it is round. If something likes the squirrel then the squirrel likes the cat. If something needs the squirrel and the squirrel is blue then it is red.
The cat is blue.
("cat" "is" "blue" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is round.
("cat" "is" "round" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If something likes the cat then the cat likes the squirrel.
((("something" "likes" "cat" "+")) -> ("cat" "likes" "squirrel" "+"))
If something is cold and it needs the squirrel then it needs the cat.
((("something" "is" "cold" "+") ("something" "needs" "squirrel" "+")) -> ("something" "needs" "cat" "+"))
If something is green then it sees the cat.
((("something" "is" "green" "+")) -> ("something" "sees" "cat" "+"))
All round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If the squirrel needs the cat then the squirrel likes the cat.
((("squirrel" "needs" "cat" "+")) -> ("squirrel" "likes" "cat" "+"))
If something is blue and it needs the squirrel then it is round.
((("something" "is" "blue" "+") ("something" "needs" "squirrel" "+")) -> ("something" "is" "round" "+"))
If something likes the squirrel then the squirrel likes the cat.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "likes" "cat" "+"))
If something needs the squirrel and the squirrel is blue then it is red.
((("something" "needs" "squirrel" "+") ("squirrel" "is" "blue" "+")) -> ("something" "is" "red" "+"))
The cat sees the squirrel.
True
1
proof
[(triple7)]
("cat" "sees" "squirrel" "+")
triple7
The squirrel does not see the cat.
False
1
inv-proof
[(triple12)]
("squirrel" "sees" "cat" "-")
triple12
The cat sees the cat.
True
2
proof
[(((triple2) -> rule3))]
("cat" "sees" "cat" "+")
((triple2) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is not cold.
False
2
inv-proof
[(((triple4) -> rule4) OR ((((triple1 triple6) -> rule6)) -> rule4))]
("cat" "is" "cold" "-")
((triple4) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((((triple1 triple6) -> (rule6 % int2))) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat needs the cat.
True
4
proof
[(((((triple4) -> rule4) triple6) -> rule2) OR ((((((triple1 triple6) -> rule6)) -> rule4) triple6) -> rule2))]
("cat" "needs" "cat" "+")
((((triple4) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
((((((triple1 triple6) -> (rule6 % int3))) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat does not need the cat.
False
4
inv-proof
[(((((triple4) -> rule4) triple6) -> rule2) OR ((((((triple1 triple6) -> rule6)) -> rule4) triple6) -> rule2))]
("cat" "needs" "cat" "-")
((((triple4) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
((((((triple1 triple6) -> (rule6 % int3))) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat is blue.[(triple1)] The cat is green.[(triple2)] The cat is red.[(triple3)] The cat is round.[(triple4 OR ((triple1 triple6) -> rule6))] The cat likes the squirrel.[(triple5 OR ((triple10) -> rule1) OR ((((triple11) -> rule5)) -> rule1))] The cat needs the squirrel.[(triple6)] The cat sees the squirrel.[(triple7)] The squirrel is red.[(triple8)] The squirrel is round.[(triple9)] The squirrel likes the cat.[(triple10 OR ((triple11) -> rule5) OR ((triple5) -> rule7))] The squirrel needs the cat.[(triple11)] The squirrel sees the cat.[(triple12)] @1: The cat is cold.[(((triple4) -> rule4) OR ((((triple1 triple6) -> rule6)) -> rule4))] The cat sees the cat.[(((triple2) -> rule3))] The squirrel is cold.[(((triple9) -> rule4))] @2: The cat needs the cat.[(((((triple4) -> rule4) triple6) -> rule2) OR ((((((triple1 triple6) -> rule6)) -> rule4) triple6) -> rule2))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat is round.
("cat" "is" "round" "+")
triple4
((triple1 triple6) -> (rule6 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple5
((triple10) -> (rule1 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
((((triple11) -> (rule5 % int2))) -> (rule1 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int2
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple6
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple7
The squirrel is red.
("squirrel" "is" "red" "+")
triple8
The squirrel is round.
("squirrel" "is" "round" "+")
triple9
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple10
((triple11) -> (rule5 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
((triple5) -> (rule7 % int1))
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple11
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple12
The cat is cold.
("cat" "is" "cold" "+")
((triple4) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
((((triple1 triple6) -> (rule6 % int2))) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple2) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple9) -> (rule4 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
((((triple4) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
((((((triple1 triple6) -> (rule6 % int3))) -> (rule4 % int2)) triple6) -> (rule2 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3