The bear is big. The bear visits the squirrel. The cat is blue. The cat visits the dog. The dog does not see the bear. The dog sees the cat. The squirrel does not need the dog. If something is big then it sees the squirrel. If something is big then it needs the squirrel. If the squirrel is not blue then the squirrel is not big. If something visits the cat and the cat visits the bear then the cat does not visit the dog. If something sees the dog and it visits the bear then it sees the cat. If something needs the squirrel then the squirrel visits the cat. If something is big and rough then it is young. If something sees the cat and the cat visits the squirrel then the squirrel needs the dog.
The bear is big.
("bear" "is" "big" "+")
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog does not see the bear.
("dog" "sees" "bear" "-")
The dog sees the cat.
("dog" "sees" "cat" "+")
The squirrel does not need the dog.
("squirrel" "needs" "dog" "-")
If something is big then it sees the squirrel.
((("something" "is" "big" "+")) -> ("something" "sees" "squirrel" "+"))
If something is big then it needs the squirrel.
((("something" "is" "big" "+")) -> ("something" "needs" "squirrel" "+"))
If the squirrel is not blue then the squirrel is not big.
((("squirrel" "is" "blue" "~")) -> ("squirrel" "is" "big" "-"))
If something visits the cat and the cat visits the bear then the cat does not visit the dog.
((("something" "visits" "cat" "+") ("cat" "visits" "bear" "+")) -> ("cat" "visits" "dog" "-"))
If something sees the dog and it visits the bear then it sees the cat.
((("something" "sees" "dog" "+") ("something" "visits" "bear" "+")) -> ("something" "sees" "cat" "+"))
If something needs the squirrel then the squirrel visits the cat.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "visits" "cat" "+"))
If something is big and rough then it is young.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something sees the cat and the cat visits the squirrel then the squirrel needs the dog.
((("something" "sees" "cat" "+") ("cat" "visits" "squirrel" "+")) -> ("squirrel" "needs" "dog" "+"))
The bear is big.
True
1
proof
[(triple1)]
("bear" "is" "big" "+")
triple1
The bear is not big.
False
1
inv-proof
[(triple1)]
("bear" "is" "big" "-")
triple1
The bear needs the squirrel.
True
2
proof
[(((triple1) -> rule2))]
("bear" "needs" "squirrel" "+")
((triple1) -> (rule2 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear does not see the squirrel.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "sees" "squirrel" "-")
((triple1) -> (rule1 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The squirrel visits the cat.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("squirrel" "visits" "cat" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The squirrel does not visit the cat.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("squirrel" "visits" "cat" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2
The squirrel does not see the cat.
Unknown
inv-rconc
[@1: The squirrel sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "sees" "cat" "-")
The cat is young.
Unknown
rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "young" "+")
The squirrel is not young.
Unknown
inv-rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "is" "young" "-")
The dog visits the squirrel.
Unknown
random
[@0: The dog visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "squirrel" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The bear is big.[(triple1)] The bear visits the squirrel.[(triple2)] The cat is blue.[(triple3)] The cat visits the dog.[(triple4)] The dog does not see the bear.[(triple5)] The dog sees the cat.[(triple6)] The squirrel does not need the dog.[(triple7)] @1: The bear needs the squirrel.[(((triple1) -> rule2))] The bear sees the squirrel.[(((triple1) -> rule1))] @2: The squirrel visits the cat.[(((((triple1) -> rule2)) -> rule6))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat visits the dog.
("cat" "visits" "dog" "+")
triple4
The dog does not see the bear.
("dog" "sees" "bear" "-")
triple5
The dog sees the cat.
("dog" "sees" "cat" "+")
triple6
The squirrel does not need the dog.
("squirrel" "needs" "dog" "-")
triple7
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((triple1) -> (rule2 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
((triple1) -> (rule1 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int2