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