The cat sees the dog. The dog eats the cat. If the cat is cold and the cat is rough then the cat needs the dog. If the cat is cold and the cat needs the dog then the dog sees the cat. If the cat sees the dog then the cat eats the dog.
The cat sees the dog.
("cat" "sees" "dog" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
If the cat is cold and the cat is rough then the cat needs the dog.
((("cat" "is" "cold" "+") ("cat" "is" "rough" "+")) -> ("cat" "needs" "dog" "+"))
If the cat is cold and the cat needs the dog then the dog sees the cat.
((("cat" "is" "cold" "+") ("cat" "needs" "dog" "+")) -> ("dog" "sees" "cat" "+"))
If the cat sees the dog then the cat eats the dog.
((("cat" "sees" "dog" "+")) -> ("cat" "eats" "dog" "+"))
The cat sees the dog.
True
1
proof
[(triple1)]
("cat" "sees" "dog" "+")
triple1
The cat does not see the dog.
False
1
inv-proof
[(triple1)]
("cat" "sees" "dog" "-")
triple1
The cat eats the dog.
True
2
proof
[(((triple1) -> rule3))]
("cat" "eats" "dog" "+")
((triple1) -> (rule3 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The cat does not eat the dog.
False
2
inv-proof
[(((triple1) -> rule3))]
("cat" "eats" "dog" "-")
((triple1) -> (rule3 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1
The cat does not need the dog.
Unknown
inv-rconc
[@1: The cat needs the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "dog" "-")
The dog sees the cat.
Unknown
rconc
[@1: The dog sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "cat" "+")
The dog does not need the cat.
Unknown
inv-random
[@0: The dog needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cat" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The cat sees the dog.[(triple1)] The dog eats the cat.[(triple2)] @1: The cat eats the dog.[(((triple1) -> rule3))]
The cat sees the dog.
("cat" "sees" "dog" "+")
triple1
The dog eats the cat.
("dog" "eats" "cat" "+")
triple2
The cat eats the dog.
("cat" "eats" "dog" "+")
((triple1) -> (rule3 % int1))
The cat eats the dog.
("cat" "eats" "dog" "+")
int1