The cat does not need the dog. The dog eats the cat. The dog needs the cat. If something visits the cat then it visits the dog. If something is red then it eats the dog. If something is young then it is red. If something is red and not round then it is big. If the cat visits the dog and the dog does not eat the cat then the dog needs the cat. If something visits the cat then it needs the dog. If something needs the cat then it is young. If something eats the cat and it needs the cat then the cat visits the dog.
The cat does not need the dog.
("cat" "needs" "dog" "-")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
If something visits the cat then it visits the dog.
((("something" "visits" "cat" "+")) -> ("something" "visits" "dog" "+"))
If something is red then it eats the dog.
((("something" "is" "red" "+")) -> ("something" "eats" "dog" "+"))
If something is young then it is red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is red and not round then it is big.
((("something" "is" "red" "+") ("something" "is" "round" "~")) -> ("something" "is" "big" "+"))
If the cat visits the dog and the dog does not eat the cat then the dog needs the cat.
((("cat" "visits" "dog" "+") ("dog" "eats" "cat" "~")) -> ("dog" "needs" "cat" "+"))
If something visits the cat then it needs the dog.
((("something" "visits" "cat" "+")) -> ("something" "needs" "dog" "+"))
If something needs the cat then it is young.
((("something" "needs" "cat" "+")) -> ("something" "is" "young" "+"))
If something eats the cat and it needs the cat then the cat visits the dog.
((("something" "eats" "cat" "+") ("something" "needs" "cat" "+")) -> ("cat" "visits" "dog" "+"))
The cat does not need the dog.
True
1
proof
[(triple1)]
("cat" "needs" "dog" "-")
triple1
The cat needs the dog.
False
1
inv-proof
[(triple1)]
("cat" "needs" "dog" "+")
triple1
The dog is young.
True
2
proof
[(((triple3) -> rule7))]
("dog" "is" "young" "+")
((triple3) -> (rule7 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is not young.
False
2
inv-proof
[(((triple3) -> rule7))]
("dog" "is" "young" "-")
((triple3) -> (rule7 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is red.
True
3
proof
[(((((triple3) -> rule7)) -> rule3))]
("dog" "is" "red" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog is not red.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule3))]
("dog" "is" "red" "-")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog eats the dog.
True
4
proof
[(((((((triple3) -> rule7)) -> rule3)) -> rule2))]
("dog" "eats" "dog" "+")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The dog does not eat the dog.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule3)) -> rule2))]
("dog" "eats" "dog" "-")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "needs" "dog" "-")
The cat eats the dog.
Unknown
rconc
[@3: The cat eats the dog.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule7 <- FAIL)]]
("cat" "eats" "dog" "+")
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 is red.
Unknown
rconc
[@2: The cat is red.[CWA. Example of deepest failure = (rule3 <- rule7 <- FAIL)]]
("cat" "is" "red" "+")
The dog does not visit the cat.
Unknown
inv-random
[@0: The dog visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "cat" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
@0: The cat does not need the dog.[(triple1)] The dog eats the cat.[(triple2)] The dog needs the cat.[(triple3)] @1: The cat visits the dog.[(((triple2 triple3) -> rule8))] The dog is young.[(((triple3) -> rule7))] @2: The dog is red.[(((((triple3) -> rule7)) -> rule3))] @3: The dog eats the dog.[(((((((triple3) -> rule7)) -> rule3)) -> rule2))]
The cat does not need the dog.
("cat" "needs" "dog" "-")
triple1
The dog eats the cat.
("dog" "eats" "cat" "+")
triple2
The dog needs the cat.
("dog" "needs" "cat" "+")
triple3
The cat visits the dog.
("cat" "visits" "dog" "+")
((triple2 triple3) -> (rule8 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((triple3) -> (rule7 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The dog is red.
("dog" "is" "red" "+")
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3