The mouse is red. The rabbit is green. The squirrel eats the tiger. The squirrel is red. The squirrel likes the mouse. The squirrel visits the mouse. The tiger visits the rabbit. If something visits the squirrel and the squirrel is red then the squirrel likes the rabbit. Red things are cold. If something likes the tiger then it likes the rabbit. If something likes the tiger and it is green then it is young. If something visits the squirrel then it likes the rabbit. If something visits the mouse and the mouse is cold then the mouse visits the squirrel.
The mouse is red.
("mouse" "is" "red" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If something visits the squirrel and the squirrel is red then the squirrel likes the rabbit.
((("something" "visits" "squirrel" "+") ("squirrel" "is" "red" "+")) -> ("squirrel" "likes" "rabbit" "+"))
Red things are cold.
((("something" "is" "red" "+")) -> ("something" "is" "cold" "+"))
If something likes the tiger then it likes the rabbit.
((("something" "likes" "tiger" "+")) -> ("something" "likes" "rabbit" "+"))
If something likes the tiger and it is green then it is young.
((("something" "likes" "tiger" "+") ("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
If something visits the squirrel then it likes the rabbit.
((("something" "visits" "squirrel" "+")) -> ("something" "likes" "rabbit" "+"))
If something visits the mouse and the mouse is cold then the mouse visits the squirrel.
((("something" "visits" "mouse" "+") ("mouse" "is" "cold" "+")) -> ("mouse" "visits" "squirrel" "+"))
The squirrel likes the mouse.
True
1
proof
[(triple5)]
("squirrel" "likes" "mouse" "+")
triple5
The squirrel does not visit the mouse.
False
1
inv-proof
[(triple6)]
("squirrel" "visits" "mouse" "-")
triple6
The squirrel is cold.
True
2
proof
[(((triple4) -> rule2))]
("squirrel" "is" "cold" "+")
((triple4) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is not cold.
False
2
inv-proof
[(((triple4) -> rule2))]
("squirrel" "is" "cold" "-")
((triple4) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The mouse visits the squirrel.
True
4
proof
[(((triple6 ((triple1) -> rule2)) -> rule6))]
("mouse" "visits" "squirrel" "+")
((triple6 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse does not visit the squirrel.
False
4
inv-proof
[(((triple6 ((triple1) -> rule2)) -> rule6))]
("mouse" "visits" "squirrel" "-")
((triple6 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The squirrel likes the rabbit.
True
6
proof
[(((((triple6 ((triple1) -> rule2)) -> rule6) triple4) -> rule1))]
("squirrel" "likes" "rabbit" "+")
((((triple6 ((triple1) -> (rule2 % int3))) -> (rule6 % int2)) triple4) -> (rule1 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The squirrel does not like the rabbit.
False
6
inv-proof
[(((((triple6 ((triple1) -> rule2)) -> rule6) triple4) -> rule1))]
("squirrel" "likes" "rabbit" "-")
((((triple6 ((triple1) -> (rule2 % int3))) -> (rule6 % int2)) triple4) -> (rule1 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The squirrel is not young.
Unknown
inv-rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "young" "-")
The rabbit is cold.
Unknown
rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "cold" "+")
The tiger is not cold.
Unknown
inv-rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "cold" "-")
The rabbit likes the rabbit.
Unknown
rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "likes" "rabbit" "+")
The rabbit does not eat the tiger.
Unknown
inv-random
[@0: The rabbit eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "tiger" "-")
The rabbit likes the mouse.
Unknown
random
[@0: The rabbit likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "mouse" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The mouse eats the tiger.
Unknown
random
[@0: The mouse eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "tiger" "+")
@0: The mouse is red.[(triple1)] The rabbit is green.[(triple2)] The squirrel eats the tiger.[(triple3)] The squirrel is red.[(triple4)] The squirrel likes the mouse.[(triple5)] The squirrel visits the mouse.[(triple6)] The tiger visits the rabbit.[(triple7)] @1: The mouse is cold.[(((triple1) -> rule2))] The squirrel is cold.[(((triple4) -> rule2))] @2: The mouse visits the squirrel.[(((triple6 ((triple1) -> rule2)) -> rule6))] @3: The mouse likes the rabbit.[(((((triple6 ((triple1) -> rule2)) -> rule6)) -> rule5))] The squirrel likes the rabbit.[(((((triple6 ((triple1) -> rule2)) -> rule6) triple4) -> rule1))]
The mouse is red.
("mouse" "is" "red" "+")
triple1
The rabbit is green.
("rabbit" "is" "green" "+")
triple2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple3
The squirrel is red.
("squirrel" "is" "red" "+")
triple4
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple5
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple6
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
((triple1) -> (rule2 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple4) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
((triple6 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((((triple6 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
((((triple6 ((triple1) -> (rule2 % int3))) -> (rule6 % int2)) triple4) -> (rule1 % int1))
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse is cold.
("mouse" "is" "cold" "+")
int3