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