The rabbit chases the tiger. The rabbit is green. The rabbit visits the tiger. The tiger chases the rabbit. The tiger is green. The tiger sees the rabbit. The tiger visits the rabbit. If something is round then it sees the tiger. If something chases the tiger and the tiger sees the rabbit then it chases the rabbit. If something sees the tiger then the tiger sees the rabbit. If something chases the rabbit and the rabbit is green then the rabbit visits the tiger. If something visits the rabbit then it visits the tiger. If something chases the rabbit and the rabbit visits the tiger then it is green.
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If something is round then it sees the tiger.
((("something" "is" "round" "+")) -> ("something" "sees" "tiger" "+"))
If something chases the tiger and the tiger sees the rabbit then it chases the rabbit.
((("something" "chases" "tiger" "+") ("tiger" "sees" "rabbit" "+")) -> ("something" "chases" "rabbit" "+"))
If something sees the tiger then the tiger sees the rabbit.
((("something" "sees" "tiger" "+")) -> ("tiger" "sees" "rabbit" "+"))
If something chases the rabbit and the rabbit is green then the rabbit visits the tiger.
((("something" "chases" "rabbit" "+") ("rabbit" "is" "green" "+")) -> ("rabbit" "visits" "tiger" "+"))
If something visits the rabbit then it visits the tiger.
((("something" "visits" "rabbit" "+")) -> ("something" "visits" "tiger" "+"))
If something chases the rabbit and the rabbit visits the tiger then it is green.
((("something" "chases" "rabbit" "+") ("rabbit" "visits" "tiger" "+")) -> ("something" "is" "green" "+"))
The rabbit visits the tiger.
True
1
proof
[(triple3 OR ((triple4 triple2) -> rule4) OR ((((triple1 triple6) -> rule2) triple2) -> rule4))]
("rabbit" "visits" "tiger" "+")
triple3
((triple4 triple2) -> (rule4 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
((((triple1 triple6) -> (rule2 % int2)) triple2) -> (rule4 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The tiger is not green.
False
1
inv-proof
[(triple5 OR ((triple4 triple3) -> rule6) OR ((triple4 ((triple4 triple2) -> rule4)) -> rule6) OR ((triple4 ((((triple1 triple6) -> rule2) triple2) -> rule4)) -> rule6))]
("tiger" "is" "green" "-")
triple5
((triple4 triple3) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((triple4 ((triple4 triple2) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
((triple4 ((((triple1 triple6) -> (rule2 % int3)) triple2) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
The rabbit chases the rabbit.
True
3
proof
[(((triple1 triple6) -> rule2))]
("rabbit" "chases" "rabbit" "+")
((triple1 triple6) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The tiger does not visit the tiger.
False
2
inv-proof
[(((triple7) -> rule5))]
("tiger" "visits" "tiger" "-")
((triple7) -> (rule5 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The rabbit does not see the tiger.
Unknown
inv-rconc
[@1: The rabbit sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "sees" "tiger" "-")
The tiger sees the tiger.
Unknown
rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The rabbit chases the tiger.[(triple1)] The rabbit is green.[(triple2 OR ((((triple1 triple6) -> rule2) triple3) -> rule6))] The rabbit visits the tiger.[(triple3 OR ((triple4 triple2) -> rule4) OR ((((triple1 triple6) -> rule2) triple2) -> rule4))] The tiger chases the rabbit.[(triple4)] The tiger is green.[(triple5 OR ((triple4 triple3) -> rule6) OR ((triple4 ((triple4 triple2) -> rule4)) -> rule6) OR ((triple4 ((((triple1 triple6) -> rule2) triple2) -> rule4)) -> rule6))] The tiger sees the rabbit.[(triple6)] The tiger visits the rabbit.[(triple7)] @1: The rabbit chases the rabbit.[(((triple1 triple6) -> rule2))] The tiger visits the tiger.[(((triple7) -> rule5))]
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple1
The rabbit is green.
("rabbit" "is" "green" "+")
triple2
((((triple1 triple6) -> (rule2 % int2)) triple3) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple3
((triple4 triple2) -> (rule4 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
((((triple1 triple6) -> (rule2 % int2)) triple2) -> (rule4 % int1))
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple4
The tiger is green.
("tiger" "is" "green" "+")
triple5
((triple4 triple3) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((triple4 ((triple4 triple2) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
((triple4 ((((triple1 triple6) -> (rule2 % int3)) triple2) -> (rule4 % int2))) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int3
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple6
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple7
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple1 triple6) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple7) -> (rule5 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1