The bear sees the cat. The cat needs the rabbit. The rabbit sees the bear. The tiger is green. If something needs the cat and the cat chases the bear then the bear chases the tiger. If something sees the tiger and it chases the tiger then the tiger is nice. If something needs the tiger then it needs the rabbit. If something chases the tiger then the tiger chases the rabbit. If something sees the tiger then the tiger chases the cat. If something chases the bear then the bear sees the cat. If the bear needs the rabbit then the rabbit sees the cat. If something needs the rabbit then the rabbit chases the bear.
The bear sees the cat.
("bear" "sees" "cat" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
The tiger is green.
("tiger" "is" "green" "+")
If something needs the cat and the cat chases the bear then the bear chases the tiger.
((("something" "needs" "cat" "+") ("cat" "chases" "bear" "+")) -> ("bear" "chases" "tiger" "+"))
If something sees the tiger and it chases the tiger then the tiger is nice.
((("something" "sees" "tiger" "+") ("something" "chases" "tiger" "+")) -> ("tiger" "is" "nice" "+"))
If something needs the tiger then it needs the rabbit.
((("something" "needs" "tiger" "+")) -> ("something" "needs" "rabbit" "+"))
If something chases the tiger then the tiger chases the rabbit.
((("something" "chases" "tiger" "+")) -> ("tiger" "chases" "rabbit" "+"))
If something sees the tiger then the tiger chases the cat.
((("something" "sees" "tiger" "+")) -> ("tiger" "chases" "cat" "+"))
If something chases the bear then the bear sees the cat.
((("something" "chases" "bear" "+")) -> ("bear" "sees" "cat" "+"))
If the bear needs the rabbit then the rabbit sees the cat.
((("bear" "needs" "rabbit" "+")) -> ("rabbit" "sees" "cat" "+"))
If something needs the rabbit then the rabbit chases the bear.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "chases" "bear" "+"))
The tiger is green.
True
1
proof
[(triple4)]
("tiger" "is" "green" "+")
triple4
The tiger is not green.
False
1
inv-proof
[(triple4)]
("tiger" "is" "green" "-")
triple4
The rabbit chases the bear.
True
2
proof
[(((triple2) -> rule8))]
("rabbit" "chases" "bear" "+")
((triple2) -> (rule8 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit does not chase the bear.
False
2
inv-proof
[(((triple2) -> rule8))]
("rabbit" "chases" "bear" "-")
((triple2) -> (rule8 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The bear does not chase the tiger.
Unknown
inv-rconc
[@1: The bear chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "chases" "tiger" "-")
The tiger is nice.
Unknown
rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "nice" "+")
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 bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bear sees the cat.[(triple1 OR ((((triple2) -> rule8)) -> rule6))] The cat needs the rabbit.[(triple2)] The rabbit sees the bear.[(triple3)] The tiger is green.[(triple4)] @1: The rabbit chases the bear.[(((triple2) -> rule8))]
The bear sees the cat.
("bear" "sees" "cat" "+")
triple1
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple2
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple3
The tiger is green.
("tiger" "is" "green" "+")
triple4
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((triple2) -> (rule8 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1