The cow visits the rabbit. The mouse eats the squirrel. The rabbit is green. The squirrel visits the mouse. If someone sees the mouse then the mouse is cold. All round, red people are big. If someone visits the rabbit then the rabbit is red. If someone is red then they are round. If someone is round and they eat the rabbit then the rabbit sees the cow. If someone visits the rabbit and they visit the cow then the cow sees the squirrel.
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If someone sees the mouse then the mouse is cold.
((("someone" "sees" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
All round, red people are big.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone visits the rabbit then the rabbit is red.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "is" "red" "+"))
If someone is red then they are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is round and they eat the rabbit then the rabbit sees the cow.
((("someone" "is" "round" "+") ("someone" "eats" "rabbit" "+")) -> ("rabbit" "sees" "cow" "+"))
If someone visits the rabbit and they visit the cow then the cow sees the squirrel.
((("someone" "visits" "rabbit" "+") ("someone" "visits" "cow" "+")) -> ("cow" "sees" "squirrel" "+"))
The squirrel visits the mouse.
True
1
proof
[(triple4)]
("squirrel" "visits" "mouse" "+")
triple4
The squirrel does not visit the mouse.
False
1
inv-proof
[(triple4)]
("squirrel" "visits" "mouse" "-")
triple4
The rabbit is red.
True
2
proof
[(((triple1) -> rule3))]
("rabbit" "is" "red" "+")
((triple1) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is not red.
False
2
inv-proof
[(((triple1) -> rule3))]
("rabbit" "is" "red" "-")
((triple1) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is round.
True
3
proof
[(((((triple1) -> rule3)) -> rule4))]
("rabbit" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is not round.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule4))]
("rabbit" "is" "round" "-")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The squirrel is not big.
Unknown
inv-rconc
[@1: The squirrel is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "big" "-")
The mouse is big.
Unknown
rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "big" "+")
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "cold" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The cow sees the mouse.
Unknown
random
[@0: The cow sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "mouse" "+")
@0: The cow visits the rabbit.[(triple1)] The mouse eats the squirrel.[(triple2)] The rabbit is green.[(triple3)] The squirrel visits the mouse.[(triple4)] @1: The rabbit is red.[(((triple1) -> rule3))] @2: The rabbit is round.[(((((triple1) -> rule3)) -> rule4))] @3: The rabbit is big.[(((((((triple1) -> rule3)) -> rule4) ((triple1) -> rule3)) -> rule2))]
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple2
The rabbit is green.
("rabbit" "is" "green" "+")
triple3
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple4
The rabbit is red.
("rabbit" "is" "red" "+")
((triple1) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3