The cat does not need the rabbit. The lion needs the rabbit. The rabbit needs the cat. The squirrel is red. If the squirrel is green and the squirrel needs the cat then the squirrel is not rough. If the rabbit needs the cat then the cat is round. If something needs the lion then the lion visits the cat.
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
If the squirrel is green and the squirrel needs the cat then the squirrel is not rough.
((("squirrel" "is" "green" "+") ("squirrel" "needs" "cat" "+")) -> ("squirrel" "is" "rough" "-"))
If the rabbit needs the cat then the cat is round.
((("rabbit" "needs" "cat" "+")) -> ("cat" "is" "round" "+"))
If something needs the lion then the lion visits the cat.
((("something" "needs" "lion" "+")) -> ("lion" "visits" "cat" "+"))
The cat does not need the rabbit.
True
1
proof
[(triple1)]
("cat" "needs" "rabbit" "-")
triple1
The rabbit does not need the cat.
False
1
inv-proof
[(triple3)]
("rabbit" "needs" "cat" "-")
triple3
The cat is round.
True
2
proof
[(((triple3) -> rule2))]
("cat" "is" "round" "+")
((triple3) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is not round.
False
2
inv-proof
[(((triple3) -> rule2))]
("cat" "is" "round" "-")
((triple3) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The lion does not visit the cat.
Unknown
inv-rconc
[@1: The lion visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "visits" "cat" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
The rabbit does not chase the cat.
Unknown
inv-random
[@0: The rabbit chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "cat" "-")
The cat chases the squirrel.
Unknown
random
[@0: The cat chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "squirrel" "+")
@0: The cat does not need the rabbit.[(triple1)] The lion needs the rabbit.[(triple2)] The rabbit needs the cat.[(triple3)] The squirrel is red.[(triple4)] @1: The cat is round.[(((triple3) -> rule2))]
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
triple1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple2
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple3
The squirrel is red.
("squirrel" "is" "red" "+")
triple4
The cat is round.
("cat" "is" "round" "+")
((triple3) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1