The bear chases the rabbit. The bear needs the tiger. The lion needs the tiger. The rabbit is blue. The rabbit needs the bear. The rabbit needs the tiger. The rabbit does not visit the tiger. The tiger is not big. The tiger is round. The tiger is young. If someone is blue then they do not chase the rabbit. If someone is blue and they do not chase the bear then they chase the rabbit.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit does not visit the tiger.
("rabbit" "visits" "tiger" "-")
The tiger is not big.
("tiger" "is" "big" "-")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
If someone is blue then they do not chase the rabbit.
((("someone" "is" "blue" "+")) -> ("someone" "chases" "rabbit" "-"))
If someone is blue and they do not chase the bear then they chase the rabbit.
((("someone" "is" "blue" "+") ("someone" "chases" "bear" "~")) -> ("someone" "chases" "rabbit" "+"))
The rabbit needs the tiger.
True
1
proof
[(triple6)]
("rabbit" "needs" "tiger" "+")
triple6
The lion does not need the tiger.
False
1
inv-proof
[(triple3)]
("lion" "needs" "tiger" "-")
triple3
The rabbit does not chase the rabbit.
True
2
proof
[(((triple4) -> rule1))]
("rabbit" "chases" "rabbit" "-")
((triple4) -> (rule1 % int1))
The rabbit does not chase the rabbit.
("rabbit" "chases" "rabbit" "-")
int1
The rabbit chases the rabbit.
False
2
inv-proof
[(((triple4) -> rule1))]
("rabbit" "chases" "rabbit" "+")
((triple4) -> (rule1 % int1))
The rabbit does not chase the rabbit.
("rabbit" "chases" "rabbit" "-")
int1
The lion does not chase the rabbit.
Unknown
inv-rconc
[@1: The lion chases the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "chases" "rabbit" "-")
The tiger chases the rabbit.
Unknown
rconc
[@1: The tiger chases the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "chases" "rabbit" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The bear chases the rabbit.[(triple1)] The bear needs the tiger.[(triple2)] The lion needs the tiger.[(triple3)] The rabbit does not visit the tiger.[(triple7)] The rabbit is blue.[(triple4)] The rabbit needs the bear.[(triple5)] The rabbit needs the tiger.[(triple6)] The tiger is not big.[(triple8)] The tiger is round.[(triple9)] The tiger is young.[(triple10)] @1: The rabbit does not chase the rabbit.[(((triple4) -> rule1))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple2
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple3
The rabbit does not visit the tiger.
("rabbit" "visits" "tiger" "-")
triple7
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple4
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple5
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple6
The tiger is not big.
("tiger" "is" "big" "-")
triple8
The tiger is round.
("tiger" "is" "round" "+")
triple9
The tiger is young.
("tiger" "is" "young" "+")
triple10
The rabbit does not chase the rabbit.
("rabbit" "chases" "rabbit" "-")
((triple4) -> (rule1 % int1))
The rabbit does not chase the rabbit.
("rabbit" "chases" "rabbit" "-")
int1