The cat is nice. The rabbit visits the cat. The squirrel is round. If someone needs the squirrel then the squirrel needs the cat. If someone is kind and they like the rabbit then the rabbit needs the cat. If someone visits the cat and they are round then the cat is nice. If someone likes the cat and the cat visits the squirrel then the cat is kind. If someone is kind and red then they like the rabbit. If the rabbit needs the cat and the cat visits the rabbit then the rabbit visits the cat. If someone is round then they need the cat. If someone needs the cat then the cat is round.
The cat is nice.
("cat" "is" "nice" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If someone needs the squirrel then the squirrel needs the cat.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "needs" "cat" "+"))
If someone is kind and they like the rabbit then the rabbit needs the cat.
((("someone" "is" "kind" "+") ("someone" "likes" "rabbit" "+")) -> ("rabbit" "needs" "cat" "+"))
If someone visits the cat and they are round then the cat is nice.
((("someone" "visits" "cat" "+") ("someone" "is" "round" "+")) -> ("cat" "is" "nice" "+"))
If someone likes the cat and the cat visits the squirrel then the cat is kind.
((("someone" "likes" "cat" "+") ("cat" "visits" "squirrel" "+")) -> ("cat" "is" "kind" "+"))
If someone is kind and red then they like the rabbit.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "likes" "rabbit" "+"))
If the rabbit needs the cat and the cat visits the rabbit then the rabbit visits the cat.
((("rabbit" "needs" "cat" "+") ("cat" "visits" "rabbit" "+")) -> ("rabbit" "visits" "cat" "+"))
If someone is round then they need the cat.
((("someone" "is" "round" "+")) -> ("someone" "needs" "cat" "+"))
If someone needs the cat then the cat is round.
((("someone" "needs" "cat" "+")) -> ("cat" "is" "round" "+"))
The cat is nice.
True
1
proof
[(triple1)]
("cat" "is" "nice" "+")
triple1
The rabbit does not visit the cat.
False
1
inv-proof
[(triple2)]
("rabbit" "visits" "cat" "-")
triple2
The squirrel needs the cat.
True
2
proof
[(((triple3) -> rule7))]
("squirrel" "needs" "cat" "+")
((triple3) -> (rule7 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The squirrel does not need the cat.
False
2
inv-proof
[(((triple3) -> rule7))]
("squirrel" "needs" "cat" "-")
((triple3) -> (rule7 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The cat is round.
True
3
proof
[(((((triple3) -> rule7)) -> rule8))]
("cat" "is" "round" "+")
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2
The cat is not round.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule8))]
("cat" "is" "round" "-")
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2
The rabbit does not like the rabbit.
Unknown
inv-rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "likes" "rabbit" "-")
The squirrel likes the rabbit.
Unknown
rconc
[@1: The squirrel likes the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "likes" "rabbit" "+")
The cat is not kind.
Unknown
inv-rconc
[@1: The cat is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "kind" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
The rabbit is not nice.
Unknown
inv-random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "-")
The rabbit likes the squirrel.
Unknown
random
[@0: The rabbit likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "squirrel" "+")
@0: The cat is nice.[(triple1)] The rabbit visits the cat.[(triple2)] The squirrel is round.[(triple3)] @1: The squirrel needs the cat.[(((triple3) -> rule7))] @2: The cat is round.[(((((triple3) -> rule7)) -> rule8))] @3: The cat needs the cat.[(((((((triple3) -> rule7)) -> rule8)) -> rule7))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple2
The squirrel is round.
("squirrel" "is" "round" "+")
triple3
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
((triple3) -> (rule7 % int1))
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
((((triple3) -> (rule7 % int2))) -> (rule8 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
((((((triple3) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
int3