The rabbit chases the squirrel. The squirrel chases the rabbit. The tiger is round. If someone chases the squirrel then they visit the rabbit. If someone is nice then they are round. Red people are rough. If someone chases the rabbit and the rabbit visits the tiger then the rabbit chases the squirrel. If someone visits the rabbit then the rabbit visits the squirrel. If someone visits the tiger then they visit the rabbit. If someone visits the squirrel then they chase the rabbit. If someone chases the squirrel then they eat the rabbit.
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone chases the squirrel then they visit the rabbit.
((("someone" "chases" "squirrel" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
Red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone chases the rabbit and the rabbit visits the tiger then the rabbit chases the squirrel.
((("someone" "chases" "rabbit" "+") ("rabbit" "visits" "tiger" "+")) -> ("rabbit" "chases" "squirrel" "+"))
If someone visits the rabbit then the rabbit visits the squirrel.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "visits" "squirrel" "+"))
If someone visits the tiger then they visit the rabbit.
((("someone" "visits" "tiger" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone visits the squirrel then they chase the rabbit.
((("someone" "visits" "squirrel" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone chases the squirrel then they eat the rabbit.
((("someone" "chases" "squirrel" "+")) -> ("someone" "eats" "rabbit" "+"))
The rabbit chases the squirrel.
True
1
proof
[(triple1)]
("rabbit" "chases" "squirrel" "+")
triple1
The tiger is not round.
False
1
inv-proof
[(triple3)]
("tiger" "is" "round" "-")
triple3
The rabbit visits the rabbit.
True
2
proof
[(((triple1) -> rule1))]
("rabbit" "visits" "rabbit" "+")
((triple1) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit does not visit the rabbit.
False
2
inv-proof
[(((triple1) -> rule1))]
("rabbit" "visits" "rabbit" "-")
((triple1) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the squirrel.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("rabbit" "visits" "squirrel" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit does not visit the squirrel.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5))]
("rabbit" "visits" "squirrel" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit is not round.
Unknown
inv-rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "round" "-")
The tiger eats the rabbit.
Unknown
rconc
[@1: The tiger eats the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "eats" "rabbit" "+")
The tiger does not visit the rabbit.
Unknown
inv-rconc
[@1: The tiger visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "visits" "rabbit" "-")
The rabbit visits the tiger.
Unknown
random
[@0: The rabbit visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "tiger" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
@0: The rabbit chases the squirrel.[(triple1)] The squirrel chases the rabbit.[(triple2)] The tiger is round.[(triple3)] @1: The rabbit eats the rabbit.[(((triple1) -> rule8))] The rabbit visits the rabbit.[(((triple1) -> rule1))] @2: The rabbit visits the squirrel.[(((((triple1) -> rule1)) -> rule5))] @3: The rabbit chases the rabbit.[(((((((triple1) -> rule1)) -> rule5)) -> rule7))]
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple1
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple2
The tiger is round.
("tiger" "is" "round" "+")
triple3
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple1) -> (rule8 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple1) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit visits the squirrel.
("rabbit" "visits" "squirrel" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int3