The cow chases the tiger. The rabbit is round. The tiger is round. If something needs the tiger then the tiger chases the cow. If something chases the tiger then the tiger chases the rabbit. If something chases the rabbit then the rabbit visits the tiger.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The tiger is round.
("tiger" "is" "round" "+")
If something needs the tiger then the tiger chases the cow.
((("something" "needs" "tiger" "+")) -> ("tiger" "chases" "cow" "+"))
If something chases the tiger then the tiger chases the rabbit.
((("something" "chases" "tiger" "+")) -> ("tiger" "chases" "rabbit" "+"))
If something chases the rabbit then the rabbit visits the tiger.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "visits" "tiger" "+"))
The rabbit is round.
True
1
proof
[(triple2)]
("rabbit" "is" "round" "+")
triple2
The rabbit is not round.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "round" "-")
triple2
The tiger chases the rabbit.
True
2
proof
[(((triple1) -> rule2))]
("tiger" "chases" "rabbit" "+")
((triple1) -> (rule2 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The tiger does not chase the rabbit.
False
2
inv-proof
[(((triple1) -> rule2))]
("tiger" "chases" "rabbit" "-")
((triple1) -> (rule2 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The rabbit visits the tiger.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("rabbit" "visits" "tiger" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The rabbit does not visit the tiger.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("rabbit" "visits" "tiger" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The tiger does not chase the cow.
Unknown
inv-rconc
[@1: The tiger chases the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "cow" "-")
The tiger needs the cow.
Unknown
random
[@0: The tiger needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "cow" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The cow does not visit the rabbit.
Unknown
inv-random
[@0: The cow visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "rabbit" "-")
The cow needs the rabbit.
Unknown
random
[@0: The cow needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "rabbit" "+")
@0: The cow chases the tiger.[(triple1)] The rabbit is round.[(triple2)] The tiger is round.[(triple3)] @1: The tiger chases the rabbit.[(((triple1) -> rule2))] @2: The rabbit visits the tiger.[(((((triple1) -> rule2)) -> rule3))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The rabbit is round.
("rabbit" "is" "round" "+")
triple2
The tiger is round.
("tiger" "is" "round" "+")
triple3
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
((triple1) -> (rule2 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2