The bear is nice. The bear needs the cat. The bear visits the lion. The cat eats the mouse. The cat is not kind. The lion does not need the bear. The lion visits the mouse. The mouse needs the bear. The mouse visits the cat. The mouse visits the lion. If something visits the mouse then it is big. If something eats the bear then the bear visits the mouse. If the lion is red then the lion is nice. Cold things are red. If something is big then it eats the bear. If something eats the lion and it is not kind then the lion does not visit the cat. If something eats the mouse and the mouse is not big then it does not eat the lion.
The bear is nice.
("bear" "is" "nice" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is not kind.
("cat" "is" "kind" "-")
The lion does not need the bear.
("lion" "needs" "bear" "-")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If something visits the mouse then it is big.
((("something" "visits" "mouse" "+")) -> ("something" "is" "big" "+"))
If something eats the bear then the bear visits the mouse.
((("something" "eats" "bear" "+")) -> ("bear" "visits" "mouse" "+"))
If the lion is red then the lion is nice.
((("lion" "is" "red" "+")) -> ("lion" "is" "nice" "+"))
Cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is big then it eats the bear.
((("something" "is" "big" "+")) -> ("something" "eats" "bear" "+"))
If something eats the lion and it is not kind then the lion does not visit the cat.
((("something" "eats" "lion" "+") ("something" "is" "kind" "~")) -> ("lion" "visits" "cat" "-"))
If something eats the mouse and the mouse is not big then it does not eat the lion.
((("something" "eats" "mouse" "+") ("mouse" "is" "big" "~")) -> ("something" "eats" "lion" "-"))
The cat eats the mouse.
True
1
proof
[(triple4)]
("cat" "eats" "mouse" "+")
triple4
The bear does not need the cat.
False
1
inv-proof
[(triple2)]
("bear" "needs" "cat" "-")
triple2
The lion is big.
True
2
proof
[(((triple7) -> rule1))]
("lion" "is" "big" "+")
((triple7) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is not big.
False
2
inv-proof
[(((triple7) -> rule1))]
("lion" "is" "big" "-")
((triple7) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion eats the bear.
True
3
proof
[(((((triple7) -> rule1)) -> rule5))]
("lion" "eats" "bear" "+")
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion does not eat the bear.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule5))]
("lion" "eats" "bear" "-")
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The bear visits the mouse.
True
4
proof
[(((((((triple7) -> rule1)) -> rule5)) -> rule2))]
("bear" "visits" "mouse" "+")
((((((triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The bear does not visit the mouse.
False
4
inv-proof
[(((((((triple7) -> rule1)) -> rule5)) -> rule2))]
("bear" "visits" "mouse" "-")
((((((triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The bear is big.
True
5
proof
[(((((((((triple7) -> rule1)) -> rule5)) -> rule2)) -> rule1))]
("bear" "is" "big" "+")
((((((((triple7) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
The lion is big.
("lion" "is" "big" "+")
int4
The bear is not big.
False
5
inv-proof
[(((((((((triple7) -> rule1)) -> rule5)) -> rule2)) -> rule1))]
("bear" "is" "big" "-")
((((((((triple7) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
The lion is big.
("lion" "is" "big" "+")
int4
The bear eats the bear.
True
6
proof
[(((((((((((triple7) -> rule1)) -> rule5)) -> rule2)) -> rule1)) -> rule5))]
("bear" "eats" "bear" "+")
((((((((((triple7) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int3
The lion eats the bear.
("lion" "eats" "bear" "+")
int4
The lion is big.
("lion" "is" "big" "+")
int5
The bear does not eat the bear.
False
6
inv-proof
[(((((((((((triple7) -> rule1)) -> rule5)) -> rule2)) -> rule1)) -> rule5))]
("bear" "eats" "bear" "-")
((((((((((triple7) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int3
The lion eats the bear.
("lion" "eats" "bear" "+")
int4
The lion is big.
("lion" "is" "big" "+")
int5
The lion is not nice.
Unknown
inv-rconc
[@2: The lion is nice.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("lion" "is" "nice" "-")
The lion is red.
Unknown
rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "red" "+")
The cat is not red.
Unknown
inv-rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "red" "-")
The mouse is big.
Unknown
rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "big" "+")
The bear is not red.
Unknown
inv-rconc
[@1: The bear is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "red" "-")
The cat eats the bear.
Unknown
rconc
[@2: The cat eats the bear.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("cat" "eats" "bear" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
The bear does not eat the cat.
Unknown
inv-random
[@0: The bear eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "cat" "-")
The bear visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The bear is nice.[(triple1)] The bear needs the cat.[(triple2)] The bear visits the lion.[(triple3)] The cat eats the mouse.[(triple4)] The cat is not kind.[(triple5)] The lion does not need the bear.[(triple6)] The lion visits the mouse.[(triple7)] The mouse needs the bear.[(triple8)] The mouse visits the cat.[(triple9)] The mouse visits the lion.[(triple10)] @1: The lion is big.[(((triple7) -> rule1))] @2: The lion eats the bear.[(((((triple7) -> rule1)) -> rule5))] @3: The bear visits the mouse.[(((((((triple7) -> rule1)) -> rule5)) -> rule2))] @4: The bear is big.[(((((((((triple7) -> rule1)) -> rule5)) -> rule2)) -> rule1))] @5: The bear eats the bear.[(((((((((((triple7) -> rule1)) -> rule5)) -> rule2)) -> rule1)) -> rule5))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The bear needs the cat.
("bear" "needs" "cat" "+")
triple2
The bear visits the lion.
("bear" "visits" "lion" "+")
triple3
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple4
The cat is not kind.
("cat" "is" "kind" "-")
triple5
The lion does not need the bear.
("lion" "needs" "bear" "-")
triple6
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple7
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple8
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple9
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple10
The lion is big.
("lion" "is" "big" "+")
((triple7) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
((((triple7) -> (rule1 % int2))) -> (rule5 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The bear visits the mouse.
("bear" "visits" "mouse" "+")
((((((triple7) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The bear is big.
("bear" "is" "big" "+")
((((((((triple7) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
The lion is big.
("lion" "is" "big" "+")
int4
The bear eats the bear.
("bear" "eats" "bear" "+")
((((((((((triple7) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear visits the mouse.
("bear" "visits" "mouse" "+")
int3
The lion eats the bear.
("lion" "eats" "bear" "+")
int4
The lion is big.
("lion" "is" "big" "+")
int5