The bear eats the lion. The dog needs the bear. The lion is cold. The lion needs the bear. The squirrel chases the bear. The squirrel is big. The squirrel needs the bear. If the squirrel chases the lion then the squirrel eats the dog. If something eats the bear then it needs the dog. If the squirrel needs the dog and the squirrel chases the lion then the dog eats the squirrel. If something is big then it chases the lion. If something chases the lion then the lion eats the bear. If something chases the squirrel then it chases the bear.
The bear eats the lion.
("bear" "eats" "lion" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
If the squirrel chases the lion then the squirrel eats the dog.
((("squirrel" "chases" "lion" "+")) -> ("squirrel" "eats" "dog" "+"))
If something eats the bear then it needs the dog.
((("something" "eats" "bear" "+")) -> ("something" "needs" "dog" "+"))
If the squirrel needs the dog and the squirrel chases the lion then the dog eats the squirrel.
((("squirrel" "needs" "dog" "+") ("squirrel" "chases" "lion" "+")) -> ("dog" "eats" "squirrel" "+"))
If something is big then it chases the lion.
((("something" "is" "big" "+")) -> ("something" "chases" "lion" "+"))
If something chases the lion then the lion eats the bear.
((("something" "chases" "lion" "+")) -> ("lion" "eats" "bear" "+"))
If something chases the squirrel then it chases the bear.
((("something" "chases" "squirrel" "+")) -> ("something" "chases" "bear" "+"))
The squirrel needs the bear.
True
1
proof
[(triple7)]
("squirrel" "needs" "bear" "+")
triple7
The squirrel does not need the bear.
False
1
inv-proof
[(triple7)]
("squirrel" "needs" "bear" "-")
triple7
The squirrel chases the lion.
True
2
proof
[(((triple6) -> rule4))]
("squirrel" "chases" "lion" "+")
((triple6) -> (rule4 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The squirrel does not chase the lion.
False
2
inv-proof
[(((triple6) -> rule4))]
("squirrel" "chases" "lion" "-")
((triple6) -> (rule4 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The lion eats the bear.
True
3
proof
[(((((triple6) -> rule4)) -> rule5))]
("lion" "eats" "bear" "+")
((((triple6) -> (rule4 % int2))) -> (rule5 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The squirrel does not eat the dog.
False
3
inv-proof
[(((((triple6) -> rule4)) -> rule1))]
("squirrel" "eats" "dog" "-")
((((triple6) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The lion needs the dog.
True
4
proof
[(((((((triple6) -> rule4)) -> rule5)) -> rule2))]
("lion" "needs" "dog" "+")
((((((triple6) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int3
The lion does not need the dog.
False
4
inv-proof
[(((((((triple6) -> rule4)) -> rule5)) -> rule2))]
("lion" "needs" "dog" "-")
((((((triple6) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int3
The bear does not chase the lion.
Unknown
inv-rconc
[@1: The bear chases the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "chases" "lion" "-")
The lion chases the bear.
Unknown
rconc
[@1: The lion chases the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "chases" "bear" "+")
The dog does not eat the squirrel.
Unknown
inv-rconc
[@2: The dog eats the squirrel.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("dog" "eats" "squirrel" "-")
The squirrel needs the dog.
Unknown
rconc
[@1: The squirrel needs the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "needs" "dog" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
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 is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
@0: The bear eats the lion.[(triple1)] The dog needs the bear.[(triple2)] The lion is cold.[(triple3)] The lion needs the bear.[(triple4)] The squirrel chases the bear.[(triple5)] The squirrel is big.[(triple6)] The squirrel needs the bear.[(triple7)] @1: The squirrel chases the lion.[(((triple6) -> rule4))] @2: The lion eats the bear.[(((((triple6) -> rule4)) -> rule5))] The squirrel eats the dog.[(((((triple6) -> rule4)) -> rule1))] @3: The lion needs the dog.[(((((((triple6) -> rule4)) -> rule5)) -> rule2))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The dog needs the bear.
("dog" "needs" "bear" "+")
triple2
The lion is cold.
("lion" "is" "cold" "+")
triple3
The lion needs the bear.
("lion" "needs" "bear" "+")
triple4
The squirrel chases the bear.
("squirrel" "chases" "bear" "+")
triple5
The squirrel is big.
("squirrel" "is" "big" "+")
triple6
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple7
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
((triple6) -> (rule4 % int1))
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
((((triple6) -> (rule4 % int2))) -> (rule5 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
((((triple6) -> (rule4 % int2))) -> (rule1 % int1))
The squirrel eats the dog.
("squirrel" "eats" "dog" "+")
int1
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int2
The lion needs the dog.
("lion" "needs" "dog" "+")
((((((triple6) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
int3