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