The cat chases the dog. The cat is green. The cat is young. The cat visits the dog. The dog chases the mouse. The dog is rough. The dog is young. The dog visits the mouse. The mouse needs the cat. The mouse visits the squirrel. The squirrel chases the dog. The squirrel needs the cat. The squirrel needs the mouse. The squirrel visits the cat. The squirrel visits the dog. If something needs the mouse then it is green. If something visits the dog and the dog chases the squirrel then the squirrel visits the cat. If something chases the mouse then it is young. If something chases the cat and it needs the squirrel then the cat is red. If the cat is young then the cat needs the squirrel. If something visits the squirrel and the squirrel is green then it needs the mouse.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is young.
("cat" "is" "young" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is young.
("dog" "is" "young" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If something needs the mouse then it is green.
((("something" "needs" "mouse" "+")) -> ("something" "is" "green" "+"))
If something visits the dog and the dog chases the squirrel then the squirrel visits the cat.
((("something" "visits" "dog" "+") ("dog" "chases" "squirrel" "+")) -> ("squirrel" "visits" "cat" "+"))
If something chases the mouse then it is young.
((("something" "chases" "mouse" "+")) -> ("something" "is" "young" "+"))
If something chases the cat and it needs the squirrel then the cat is red.
((("something" "chases" "cat" "+") ("something" "needs" "squirrel" "+")) -> ("cat" "is" "red" "+"))
If the cat is young then the cat needs the squirrel.
((("cat" "is" "young" "+")) -> ("cat" "needs" "squirrel" "+"))
If something visits the squirrel and the squirrel is green then it needs the mouse.
((("something" "visits" "squirrel" "+") ("squirrel" "is" "green" "+")) -> ("something" "needs" "mouse" "+"))
The cat is green.
True
1
proof
[(triple2)]
("cat" "is" "green" "+")
triple2
The cat is not green.
False
1
inv-proof
[(triple2)]
("cat" "is" "green" "-")
triple2
The squirrel is green.
True
2
proof
[(((triple13) -> rule1))]
("squirrel" "is" "green" "+")
((triple13) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is not green.
False
2
inv-proof
[(((triple13) -> rule1))]
("squirrel" "is" "green" "-")
((triple13) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The mouse needs the mouse.
True
4
proof
[(((triple10 ((triple13) -> rule1)) -> rule6))]
("mouse" "needs" "mouse" "+")
((triple10 ((triple13) -> (rule1 % int2))) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The mouse does not need the mouse.
False
4
inv-proof
[(((triple10 ((triple13) -> rule1)) -> rule6))]
("mouse" "needs" "mouse" "-")
((triple10 ((triple13) -> (rule1 % int2))) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The mouse is green.
True
5
proof
[(((((triple10 ((triple13) -> rule1)) -> rule6)) -> rule1))]
("mouse" "is" "green" "+")
((((triple10 ((triple13) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The mouse is not green.
False
5
inv-proof
[(((((triple10 ((triple13) -> rule1)) -> rule6)) -> rule1))]
("mouse" "is" "green" "-")
((((triple10 ((triple13) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The dog is not green.
Unknown
inv-rconc
[@2: The dog is green.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("dog" "is" "green" "-")
The cat is red.
Unknown
rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "red" "+")
The squirrel is not young.
Unknown
inv-rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "young" "-")
The cat needs the mouse.
Unknown
rconc
[@1: The cat needs the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "needs" "mouse" "+")
The squirrel does not chase the mouse.
Unknown
inv-random
[@0: The squirrel chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "mouse" "-")
The dog visits the cat.
Unknown
random
[@0: The dog visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "cat" "+")
The squirrel is not round.
Unknown
inv-random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "-")
The dog chases the squirrel.
Unknown
random
[@0: The dog chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "squirrel" "+")
@0: The cat chases the dog.[(triple1)] The cat is green.[(triple2)] The cat is young.[(triple3)] The cat visits the dog.[(triple4)] The dog chases the mouse.[(triple5)] The dog is rough.[(triple6)] The dog is young.[(triple7 OR ((triple5) -> rule3))] The dog visits the mouse.[(triple8)] The mouse needs the cat.[(triple9)] The mouse visits the squirrel.[(triple10)] The squirrel chases the dog.[(triple11)] The squirrel needs the cat.[(triple12)] The squirrel needs the mouse.[(triple13)] The squirrel visits the cat.[(triple14)] The squirrel visits the dog.[(triple15)] @1: The cat needs the squirrel.[(((triple3) -> rule5))] The squirrel is green.[(((triple13) -> rule1))] @2: The mouse needs the mouse.[(((triple10 ((triple13) -> rule1)) -> rule6))] @3: The mouse is green.[(((((triple10 ((triple13) -> rule1)) -> rule6)) -> rule1))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is young.
("cat" "is" "young" "+")
triple3
The cat visits the dog.
("cat" "visits" "dog" "+")
triple4
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple5
The dog is rough.
("dog" "is" "rough" "+")
triple6
The dog is young.
("dog" "is" "young" "+")
triple7
((triple5) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple8
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple9
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple10
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple11
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple12
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple13
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple14
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple15
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
((triple3) -> (rule5 % int1))
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
((triple13) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple10 ((triple13) -> (rule1 % int2))) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The mouse is green.
("mouse" "is" "green" "+")
((((triple10 ((triple13) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3