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