The cat does not need the rabbit. The cat does not see the rabbit. The rabbit is red. The rabbit is round. The rabbit needs the cat. The rabbit sees the cat. The rabbit visits the cat. If someone visits the cat then they are big. If someone visits the rabbit and they are not green then the rabbit is big.
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is 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" "+")
If someone visits the cat then they are big.
((("someone" "visits" "cat" "+")) -> ("someone" "is" "big" "+"))
If someone visits the rabbit and they are not green then the rabbit is big.
((("someone" "visits" "rabbit" "+") ("someone" "is" "green" "~")) -> ("rabbit" "is" "big" "+"))
The rabbit sees the cat.
True
1
proof
[(triple6)]
("rabbit" "sees" "cat" "+")
triple6
The cat needs the rabbit.
False
1
inv-proof
[(triple1)]
("cat" "needs" "rabbit" "+")
triple1
The rabbit is big.
True
2
proof
[(((triple7) -> rule1))]
("rabbit" "is" "big" "+")
((triple7) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is not big.
False
2
inv-proof
[(((triple7) -> rule1))]
("rabbit" "is" "big" "-")
((triple7) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The cat is not big.
Unknown
inv-rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "big" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The cat does not need the rabbit.[(triple1)] The cat does not see the rabbit.[(triple2)] The rabbit is red.[(triple3)] The rabbit is round.[(triple4)] The rabbit needs the cat.[(triple5)] The rabbit sees the cat.[(triple6)] The rabbit visits the cat.[(triple7)] @1: The rabbit is big.[(((triple7) -> rule1))]
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
triple1
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
triple2
The rabbit is red.
("rabbit" "is" "red" "+")
triple3
The rabbit is round.
("rabbit" "is" "round" "+")
triple4
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple5
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple6
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple7
The rabbit is big.
("rabbit" "is" "big" "+")
((triple7) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1