The mouse eats the squirrel. The mouse sees the squirrel. The rabbit eats the mouse. The rabbit is big. The rabbit is cold. The rabbit is round. The rabbit sees the mouse. The rabbit sees the squirrel. The rabbit visits the mouse. The squirrel is nice. The squirrel is round. The squirrel sees the mouse. If something is nice then it sees the rabbit. If something is nice and it sees the rabbit then it visits the rabbit.
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If something is nice then it sees the rabbit.
((("something" "is" "nice" "+")) -> ("something" "sees" "rabbit" "+"))
If something is nice and it sees the rabbit then it visits the rabbit.
((("something" "is" "nice" "+") ("something" "sees" "rabbit" "+")) -> ("something" "visits" "rabbit" "+"))
The rabbit is big.
True
1
proof
[(triple4)]
("rabbit" "is" "big" "+")
triple4
The rabbit is not big.
False
1
inv-proof
[(triple4)]
("rabbit" "is" "big" "-")
triple4
The squirrel sees the rabbit.
True
2
proof
[(((triple10) -> rule1))]
("squirrel" "sees" "rabbit" "+")
((triple10) -> (rule1 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The squirrel does not see the rabbit.
False
2
inv-proof
[(((triple10) -> rule1))]
("squirrel" "sees" "rabbit" "-")
((triple10) -> (rule1 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The squirrel visits the rabbit.
True
4
proof
[(((triple10 ((triple10) -> rule1)) -> rule2))]
("squirrel" "visits" "rabbit" "+")
((triple10 ((triple10) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2
The squirrel does not visit the rabbit.
False
4
inv-proof
[(((triple10 ((triple10) -> rule1)) -> rule2))]
("squirrel" "visits" "rabbit" "-")
((triple10 ((triple10) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2
The mouse does not visit the rabbit.
Unknown
inv-rconc
[@1: The mouse visits the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "visits" "rabbit" "-")
The rabbit visits the rabbit.
Unknown
rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "visits" "rabbit" "+")
The mouse does not see the rabbit.
Unknown
inv-rconc
[@1: The mouse sees the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "rabbit" "-")
The squirrel eats the rabbit.
Unknown
random
[@0: The squirrel eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "rabbit" "+")
The squirrel is not kind.
Unknown
inv-random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The mouse eats the squirrel.[(triple1)] The mouse sees the squirrel.[(triple2)] The rabbit eats the mouse.[(triple3)] The rabbit is big.[(triple4)] The rabbit is cold.[(triple5)] The rabbit is round.[(triple6)] The rabbit sees the mouse.[(triple7)] The rabbit sees the squirrel.[(triple8)] The rabbit visits the mouse.[(triple9)] The squirrel is nice.[(triple10)] The squirrel is round.[(triple11)] The squirrel sees the mouse.[(triple12)] @1: The squirrel sees the rabbit.[(((triple10) -> rule1))] @2: The squirrel visits the rabbit.[(((triple10 ((triple10) -> rule1)) -> rule2))]
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple3
The rabbit is big.
("rabbit" "is" "big" "+")
triple4
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple5
The rabbit is round.
("rabbit" "is" "round" "+")
triple6
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple7
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple8
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple9
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple10
The squirrel is round.
("squirrel" "is" "round" "+")
triple11
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple12
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
((triple10) -> (rule1 % int1))
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
((triple10 ((triple10) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
int2