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