The bear is cold. The bear needs the dog. The bear sees the squirrel. The cow chases the dog. The cow is cold. The cow is not red. The cow needs the squirrel. The dog is big. The dog sees the squirrel. The squirrel is round. If something chases the bear and it is not cold then the bear does not chase the dog. If the squirrel is cold then the squirrel is big. If something sees the bear and it needs the bear then the bear chases the squirrel. If the cow needs the squirrel and the squirrel is round then the squirrel sees the cow. If something sees the bear and it chases the bear then the bear needs the dog. If something is round and it sees the cow then it needs the cow.
The bear is cold.
("bear" "is" "cold" "+")
The bear needs the dog.
("bear" "needs" "dog" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is not red.
("cow" "is" "red" "-")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The dog is big.
("dog" "is" "big" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If something chases the bear and it is not cold then the bear does not chase the dog.
((("something" "chases" "bear" "+") ("something" "is" "cold" "~")) -> ("bear" "chases" "dog" "-"))
If the squirrel is cold then the squirrel is big.
((("squirrel" "is" "cold" "+")) -> ("squirrel" "is" "big" "+"))
If something sees the bear and it needs the bear then the bear chases the squirrel.
((("something" "sees" "bear" "+") ("something" "needs" "bear" "+")) -> ("bear" "chases" "squirrel" "+"))
If the cow needs the squirrel and the squirrel is round then the squirrel sees the cow.
((("cow" "needs" "squirrel" "+") ("squirrel" "is" "round" "+")) -> ("squirrel" "sees" "cow" "+"))
If something sees the bear and it chases the bear then the bear needs the dog.
((("something" "sees" "bear" "+") ("something" "chases" "bear" "+")) -> ("bear" "needs" "dog" "+"))
If something is round and it sees the cow then it needs the cow.
((("something" "is" "round" "+") ("something" "sees" "cow" "+")) -> ("something" "needs" "cow" "+"))
The cow chases the dog.
True
1
proof
[(triple4)]
("cow" "chases" "dog" "+")
triple4
The cow is not cold.
False
1
inv-proof
[(triple5)]
("cow" "is" "cold" "-")
triple5
The squirrel sees the cow.
True
3
proof
[(((triple7 triple10) -> rule4))]
("squirrel" "sees" "cow" "+")
((triple7 triple10) -> (rule4 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel does not see the cow.
False
3
inv-proof
[(((triple7 triple10) -> rule4))]
("squirrel" "sees" "cow" "-")
((triple7 triple10) -> (rule4 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel needs the cow.
True
5
proof
[(((triple10 ((triple7 triple10) -> rule4)) -> rule6))]
("squirrel" "needs" "cow" "+")
((triple10 ((triple7 triple10) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The squirrel does not need the cow.
False
5
inv-proof
[(((triple10 ((triple7 triple10) -> rule4)) -> rule6))]
("squirrel" "needs" "cow" "-")
((triple10 ((triple7 triple10) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The bear does not chase the squirrel.
Unknown
inv-rconc
[@1: The bear chases the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "chases" "squirrel" "-")
The squirrel is big.
Unknown
rconc
[@1: The squirrel is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "big" "+")
The bear does not need the cow.
Unknown
inv-rconc
[@1: The bear needs the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "needs" "cow" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The dog does not see the cow.
Unknown
inv-random
[@0: The dog sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cow" "-")
The bear needs the squirrel.
Unknown
random
[@0: The bear needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "squirrel" "+")
@0: The bear is cold.[(triple1)] The bear needs the dog.[(triple2)] The bear sees the squirrel.[(triple3)] The cow chases the dog.[(triple4)] The cow is cold.[(triple5)] The cow is not red.[(triple6)] The cow needs the squirrel.[(triple7)] The dog is big.[(triple8)] The dog sees the squirrel.[(triple9)] The squirrel is round.[(triple10)] @1: The squirrel sees the cow.[(((triple7 triple10) -> rule4))] @2: The squirrel needs the cow.[(((triple10 ((triple7 triple10) -> rule4)) -> rule6))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear needs the dog.
("bear" "needs" "dog" "+")
triple2
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple3
The cow chases the dog.
("cow" "chases" "dog" "+")
triple4
The cow is cold.
("cow" "is" "cold" "+")
triple5
The cow is not red.
("cow" "is" "red" "-")
triple6
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple7
The dog is big.
("dog" "is" "big" "+")
triple8
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple9
The squirrel is round.
("squirrel" "is" "round" "+")
triple10
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
((triple7 triple10) -> (rule4 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
((triple10 ((triple7 triple10) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2