The cat needs the tiger. The rabbit is not big. The squirrel sees the tiger. The tiger does not need the cat. If the rabbit is red and the rabbit sees the cat then the cat needs the rabbit. If someone visits the squirrel then they are blue. If someone sees the tiger then they visit the squirrel. If someone needs the cat then they visit the cat. If someone visits the rabbit and they are blue then the rabbit is not red. If someone visits the cat then the cat sees the tiger.
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The rabbit is not big.
("rabbit" "is" "big" "-")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger does not need the cat.
("tiger" "needs" "cat" "-")
If the rabbit is red and the rabbit sees the cat then the cat needs the rabbit.
((("rabbit" "is" "red" "+") ("rabbit" "sees" "cat" "+")) -> ("cat" "needs" "rabbit" "+"))
If someone visits the squirrel then they are blue.
((("someone" "visits" "squirrel" "+")) -> ("someone" "is" "blue" "+"))
If someone sees the tiger then they visit the squirrel.
((("someone" "sees" "tiger" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone needs the cat then they visit the cat.
((("someone" "needs" "cat" "+")) -> ("someone" "visits" "cat" "+"))
If someone visits the rabbit and they are blue then the rabbit is not red.
((("someone" "visits" "rabbit" "+") ("someone" "is" "blue" "+")) -> ("rabbit" "is" "red" "-"))
If someone visits the cat then the cat sees the tiger.
((("someone" "visits" "cat" "+")) -> ("cat" "sees" "tiger" "+"))
The rabbit is not big.
True
1
proof
[(triple2)]
("rabbit" "is" "big" "-")
triple2
The cat does not need the tiger.
False
1
inv-proof
[(triple1)]
("cat" "needs" "tiger" "-")
triple1
The squirrel visits the squirrel.
True
2
proof
[(((triple3) -> rule3))]
("squirrel" "visits" "squirrel" "+")
((triple3) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel does not visit the squirrel.
False
2
inv-proof
[(((triple3) -> rule3))]
("squirrel" "visits" "squirrel" "-")
((triple3) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is blue.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("squirrel" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel is not blue.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("squirrel" "is" "blue" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The cat is not blue.
Unknown
inv-rconc
[@4: The cat is blue.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule6 <- rule4 <- FAIL)]]
("cat" "is" "blue" "-")
The cat visits the squirrel.
Unknown
rconc
[@3: The cat visits the squirrel.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule4 <- FAIL)]]
("cat" "visits" "squirrel" "+")
The cat does not need the rabbit.
Unknown
inv-rconc
[@1: The cat needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "rabbit" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The rabbit does not see the squirrel.
Unknown
inv-random
[@0: The rabbit sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "squirrel" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The cat needs the tiger.[(triple1)] The rabbit is not big.[(triple2)] The squirrel sees the tiger.[(triple3)] The tiger does not need the cat.[(triple4)] @1: The squirrel visits the squirrel.[(((triple3) -> rule3))] @2: The squirrel is blue.[(((((triple3) -> rule3)) -> rule2))]
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple1
The rabbit is not big.
("rabbit" "is" "big" "-")
triple2
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple3
The tiger does not need the cat.
("tiger" "needs" "cat" "-")
triple4
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple3) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2