The cat chases the rabbit. The mouse is big. The rabbit needs the tiger. The tiger sees the cat. If the cat chases the rabbit and the rabbit chases the cat then the rabbit sees the cat. If something chases the tiger then it needs the cat. If something needs the tiger then it chases the cat.
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If the cat chases the rabbit and the rabbit chases the cat then the rabbit sees the cat.
((("cat" "chases" "rabbit" "+") ("rabbit" "chases" "cat" "+")) -> ("rabbit" "sees" "cat" "+"))
If something chases the tiger then it needs the cat.
((("something" "chases" "tiger" "+")) -> ("something" "needs" "cat" "+"))
If something needs the tiger then it chases the cat.
((("something" "needs" "tiger" "+")) -> ("something" "chases" "cat" "+"))
The rabbit needs the tiger.
True
1
proof
[(triple3)]
("rabbit" "needs" "tiger" "+")
triple3
The tiger does not see the cat.
False
1
inv-proof
[(triple4)]
("tiger" "sees" "cat" "-")
triple4
The rabbit chases the cat.
True
2
proof
[(((triple3) -> rule3))]
("rabbit" "chases" "cat" "+")
((triple3) -> (rule3 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The rabbit does not chase the cat.
False
2
inv-proof
[(((triple3) -> rule3))]
("rabbit" "chases" "cat" "-")
((triple3) -> (rule3 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The rabbit sees the cat.
True
4
proof
[(((triple1 ((triple3) -> rule3)) -> rule1))]
("rabbit" "sees" "cat" "+")
((triple1 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int2
The rabbit does not see the cat.
False
4
inv-proof
[(((triple1 ((triple3) -> rule3)) -> rule1))]
("rabbit" "sees" "cat" "-")
((triple1 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int2
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "needs" "cat" "-")
The rabbit needs the cat.
Unknown
rconc
[@1: The rabbit needs the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "needs" "cat" "+")
The mouse does not need the cat.
Unknown
inv-rconc
[@1: The mouse needs the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "cat" "-")
The mouse chases the tiger.
Unknown
random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "+")
The tiger is not nice.
Unknown
inv-random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "-")
The mouse chases the rabbit.
Unknown
random
[@0: The mouse chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "rabbit" "+")
@0: The cat chases the rabbit.[(triple1)] The mouse is big.[(triple2)] The rabbit needs the tiger.[(triple3)] The tiger sees the cat.[(triple4)] @1: The rabbit chases the cat.[(((triple3) -> rule3))] @2: The rabbit sees the cat.[(((triple1 ((triple3) -> rule3)) -> rule1))]
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple3
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple4
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
((triple3) -> (rule3 % int1))
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((triple1 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
int2