The bear likes the cat. The cat visits the bear. The mouse sees the squirrel. The squirrel visits the bear. If something visits the squirrel then it sees the squirrel. If something visits the bear and it is red then it likes the mouse. If something visits the bear then it visits the squirrel. If something likes the bear then it visits the cat. If something sees the mouse and it visits the mouse then the mouse is cold. If something sees the squirrel and it visits the bear then it likes the squirrel.
The bear likes the cat.
("bear" "likes" "cat" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
If something visits the squirrel then it sees the squirrel.
((("something" "visits" "squirrel" "+")) -> ("something" "sees" "squirrel" "+"))
If something visits the bear and it is red then it likes the mouse.
((("something" "visits" "bear" "+") ("something" "is" "red" "+")) -> ("something" "likes" "mouse" "+"))
If something visits the bear then it visits the squirrel.
((("something" "visits" "bear" "+")) -> ("something" "visits" "squirrel" "+"))
If something likes the bear then it visits the cat.
((("something" "likes" "bear" "+")) -> ("something" "visits" "cat" "+"))
If something sees the mouse and it visits the mouse then the mouse is cold.
((("something" "sees" "mouse" "+") ("something" "visits" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
If something sees the squirrel and it visits the bear then it likes the squirrel.
((("something" "sees" "squirrel" "+") ("something" "visits" "bear" "+")) -> ("something" "likes" "squirrel" "+"))
The cat visits the bear.
True
1
proof
[(triple2)]
("cat" "visits" "bear" "+")
triple2
The bear does not like the cat.
False
1
inv-proof
[(triple1)]
("bear" "likes" "cat" "-")
triple1
The cat visits the squirrel.
True
2
proof
[(((triple2) -> rule3))]
("cat" "visits" "squirrel" "+")
((triple2) -> (rule3 % int1))
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int1
The squirrel does not visit the squirrel.
False
2
inv-proof
[(((triple4) -> rule3))]
("squirrel" "visits" "squirrel" "-")
((triple4) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The cat sees the squirrel.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("cat" "sees" "squirrel" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The squirrel does not see the squirrel.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule1))]
("squirrel" "sees" "squirrel" "-")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The cat likes the squirrel.
True
5
proof
[(((((((triple2) -> rule3)) -> rule1) triple2) -> rule6))]
("cat" "likes" "squirrel" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2)) triple2) -> (rule6 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int3
The squirrel does not like the squirrel.
False
5
inv-proof
[(((((((triple4) -> rule3)) -> rule1) triple4) -> rule6))]
("squirrel" "likes" "squirrel" "-")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3
The mouse does not like the mouse.
Unknown
inv-rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse likes the squirrel.
Unknown
rconc
[@1: The mouse likes the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "likes" "squirrel" "+")
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "cold" "-")
The squirrel likes the mouse.
Unknown
rconc
[@1: The squirrel likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "likes" "mouse" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
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 kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The bear likes the cat.[(triple1)] The cat visits the bear.[(triple2)] The mouse sees the squirrel.[(triple3)] The squirrel visits the bear.[(triple4)] @1: The cat visits the squirrel.[(((triple2) -> rule3))] The squirrel visits the squirrel.[(((triple4) -> rule3))] @2: The cat sees the squirrel.[(((((triple2) -> rule3)) -> rule1))] The squirrel sees the squirrel.[(((((triple4) -> rule3)) -> rule1))] @3: The cat likes the squirrel.[(((((((triple2) -> rule3)) -> rule1) triple2) -> rule6))] The squirrel likes the squirrel.[(((((((triple4) -> rule3)) -> rule1) triple4) -> rule6))]
The bear likes the cat.
("bear" "likes" "cat" "+")
triple1
The cat visits the bear.
("cat" "visits" "bear" "+")
triple2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple3
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple4
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
((triple2) -> (rule3 % int1))
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple4) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2)) triple2) -> (rule6 % int1))
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
int1
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int3
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((((((triple4) -> (rule3 % int3))) -> (rule1 % int2)) triple4) -> (rule6 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int3