The bear is big. The lion visits the rabbit. The rabbit eats the lion. The squirrel is big. If something is red then it needs the lion. If something needs the rabbit and it needs the squirrel then the rabbit is rough. If something is rough and it eats the rabbit then it eats the lion. If something is big and it needs the lion then the lion needs the rabbit. Big things are red. If something visits the lion then it visits the bear.
The bear is big.
("bear" "is" "big" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
If something is red then it needs the lion.
((("something" "is" "red" "+")) -> ("something" "needs" "lion" "+"))
If something needs the rabbit and it needs the squirrel then the rabbit is rough.
((("something" "needs" "rabbit" "+") ("something" "needs" "squirrel" "+")) -> ("rabbit" "is" "rough" "+"))
If something is rough and it eats the rabbit then it eats the lion.
((("something" "is" "rough" "+") ("something" "eats" "rabbit" "+")) -> ("something" "eats" "lion" "+"))
If something is big and it needs the lion then the lion needs the rabbit.
((("something" "is" "big" "+") ("something" "needs" "lion" "+")) -> ("lion" "needs" "rabbit" "+"))
Big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something visits the lion then it visits the bear.
((("something" "visits" "lion" "+")) -> ("something" "visits" "bear" "+"))
The bear is big.
True
1
proof
[(triple1)]
("bear" "is" "big" "+")
triple1
The squirrel is not big.
False
1
inv-proof
[(triple4)]
("squirrel" "is" "big" "-")
triple4
The squirrel is red.
True
2
proof
[(((triple4) -> rule5))]
("squirrel" "is" "red" "+")
((triple4) -> (rule5 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is not red.
False
2
inv-proof
[(((triple4) -> rule5))]
("squirrel" "is" "red" "-")
((triple4) -> (rule5 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel needs the lion.
True
3
proof
[(((((triple4) -> rule5)) -> rule1))]
("squirrel" "needs" "lion" "+")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The bear does not need the lion.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule1))]
("bear" "needs" "lion" "-")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The lion needs the rabbit.
True
5
proof
[(((triple1 ((((triple1) -> rule5)) -> rule1)) -> rule4) OR ((triple4 ((((triple4) -> rule5)) -> rule1)) -> rule4))]
("lion" "needs" "rabbit" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
((triple4 ((((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The lion does not need the rabbit.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule5)) -> rule1)) -> rule4) OR ((triple4 ((((triple4) -> rule5)) -> rule1)) -> rule4))]
("lion" "needs" "rabbit" "-")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
((triple4 ((((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The rabbit does not need the lion.
Unknown
inv-rconc
[@2: The rabbit needs the lion.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("rabbit" "needs" "lion" "-")
The bear eats the lion.
Unknown
rconc
[@1: The bear eats the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "eats" "lion" "+")
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "visits" "bear" "-")
The lion visits the bear.
Unknown
rconc
[@1: The lion visits the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "visits" "bear" "+")
The squirrel does not need the rabbit.
Unknown
inv-random
[@0: The squirrel needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "rabbit" "-")
The bear is nice.
Unknown
random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "+")
The bear does not need the squirrel.
Unknown
inv-random
[@0: The bear needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "squirrel" "-")
The rabbit needs the squirrel.
Unknown
random
[@0: The rabbit needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "squirrel" "+")
@0: The bear is big.[(triple1)] The lion visits the rabbit.[(triple2)] The rabbit eats the lion.[(triple3)] The squirrel is big.[(triple4)] @1: The bear is red.[(((triple1) -> rule5))] The squirrel is red.[(((triple4) -> rule5))] @2: The bear needs the lion.[(((((triple1) -> rule5)) -> rule1))] The squirrel needs the lion.[(((((triple4) -> rule5)) -> rule1))] @3: The lion needs the rabbit.[(((triple1 ((((triple1) -> rule5)) -> rule1)) -> rule4) OR ((triple4 ((((triple4) -> rule5)) -> rule1)) -> rule4))]
The bear is big.
("bear" "is" "big" "+")
triple1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple2
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple3
The squirrel is big.
("squirrel" "is" "big" "+")
triple4
The bear is red.
("bear" "is" "red" "+")
((triple1) -> (rule5 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
((triple4) -> (rule5 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear is red.
("bear" "is" "red" "+")
int2
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The bear is red.
("bear" "is" "red" "+")
int3
((triple4 ((((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3