The cat likes the squirrel. The squirrel is blue. The squirrel sees the cat. If the cat sees the squirrel then the cat eats the squirrel. If something likes the squirrel and it likes the cat then the cat sees the squirrel. If something sees the cat and the cat is cold then the cat likes the squirrel. If something likes the squirrel then it is round. If something is red then it likes the squirrel. If something likes the squirrel and the squirrel sees the cat then the cat is red. If something is red then it sees the squirrel. If something likes the squirrel then it eats the cat.
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If the cat sees the squirrel then the cat eats the squirrel.
((("cat" "sees" "squirrel" "+")) -> ("cat" "eats" "squirrel" "+"))
If something likes the squirrel and it likes the cat then the cat sees the squirrel.
((("something" "likes" "squirrel" "+") ("something" "likes" "cat" "+")) -> ("cat" "sees" "squirrel" "+"))
If something sees the cat and the cat is cold then the cat likes the squirrel.
((("something" "sees" "cat" "+") ("cat" "is" "cold" "+")) -> ("cat" "likes" "squirrel" "+"))
If something likes the squirrel then it is round.
((("something" "likes" "squirrel" "+")) -> ("something" "is" "round" "+"))
If something is red then it likes the squirrel.
((("something" "is" "red" "+")) -> ("something" "likes" "squirrel" "+"))
If something likes the squirrel and the squirrel sees the cat then the cat is red.
((("something" "likes" "squirrel" "+") ("squirrel" "sees" "cat" "+")) -> ("cat" "is" "red" "+"))
If something is red then it sees the squirrel.
((("something" "is" "red" "+")) -> ("something" "sees" "squirrel" "+"))
If something likes the squirrel then it eats the cat.
((("something" "likes" "squirrel" "+")) -> ("something" "eats" "cat" "+"))
The cat likes the squirrel.
True
1
proof
[(triple1)]
("cat" "likes" "squirrel" "+")
triple1
The squirrel does not see the cat.
False
1
inv-proof
[(triple3)]
("squirrel" "sees" "cat" "-")
triple3
The cat eats the cat.
True
2
proof
[(((triple1) -> rule8))]
("cat" "eats" "cat" "+")
((triple1) -> (rule8 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is not red.
False
3
inv-proof
[(((triple1 triple3) -> rule6))]
("cat" "is" "red" "-")
((triple1 triple3) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat sees the squirrel.
True
4
proof
[(((((triple1 triple3) -> rule6)) -> rule7))]
("cat" "sees" "squirrel" "+")
((((triple1 triple3) -> (rule6 % int2))) -> (rule7 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat does not see the squirrel.
False
4
inv-proof
[(((((triple1 triple3) -> rule6)) -> rule7))]
("cat" "sees" "squirrel" "-")
((((triple1 triple3) -> (rule6 % int2))) -> (rule7 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat eats the squirrel.
True
5
proof
[(((((((triple1 triple3) -> rule6)) -> rule7)) -> rule1))]
("cat" "eats" "squirrel" "+")
((((((triple1 triple3) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat does not eat the squirrel.
False
5
inv-proof
[(((((((triple1 triple3) -> rule6)) -> rule7)) -> rule1))]
("cat" "eats" "squirrel" "-")
((((((triple1 triple3) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The squirrel does not like the squirrel.
Unknown
inv-rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "likes" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel does not eat the cat.
Unknown
inv-rconc
[@2: The squirrel eats the cat.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("squirrel" "eats" "cat" "-")
The squirrel is round.
Unknown
rconc
[@2: The squirrel is round.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("squirrel" "is" "round" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
The squirrel is not cold.
Unknown
inv-random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat likes the squirrel.[(triple1)] The squirrel is blue.[(triple2)] The squirrel sees the cat.[(triple3)] @1: The cat eats the cat.[(((triple1) -> rule8))] The cat is red.[(((triple1 triple3) -> rule6))] The cat is round.[(((triple1) -> rule4))] @2: The cat sees the squirrel.[(((((triple1 triple3) -> rule6)) -> rule7))] @3: The cat eats the squirrel.[(((((((triple1 triple3) -> rule6)) -> rule7)) -> rule1))]
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple1
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple2
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple3
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple1) -> (rule8 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
((triple1 triple3) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((triple1) -> (rule4 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
((((triple1 triple3) -> (rule6 % int2))) -> (rule7 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
((((((triple1 triple3) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3