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