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