The rabbit is big. The squirrel does not need the rabbit. If something is young then it needs the squirrel. If something is big then it sees the squirrel.
The rabbit is big.
("rabbit" "is" "big" "+")
The squirrel does not need the rabbit.
("squirrel" "needs" "rabbit" "-")
If something is young then it needs the squirrel.
((("something" "is" "young" "+")) -> ("something" "needs" "squirrel" "+"))
If something is big then it sees the squirrel.
((("something" "is" "big" "+")) -> ("something" "sees" "squirrel" "+"))
The squirrel does not need the rabbit.
True
1
proof
[(triple2)]
("squirrel" "needs" "rabbit" "-")
triple2
The rabbit is not big.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "big" "-")
triple1
The rabbit sees the squirrel.
True
2
proof
[(((triple1) -> rule2))]
("rabbit" "sees" "squirrel" "+")
((triple1) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The rabbit does not see the squirrel.
False
2
inv-proof
[(((triple1) -> rule2))]
("rabbit" "sees" "squirrel" "-")
((triple1) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The rabbit is big.[(triple1)] The squirrel does not need the rabbit.[(triple2)] @1: The rabbit sees the squirrel.[(((triple1) -> rule2))]
The rabbit is big.
("rabbit" "is" "big" "+")
triple1
The squirrel does not need the rabbit.
("squirrel" "needs" "rabbit" "-")
triple2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
((triple1) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1