The cat is big. The dog needs the cat. If someone visits the cat then the cat does not eat the dog. If someone is green then they need the dog. If someone visits the dog then the dog visits the cat. If someone needs the dog then the dog eats the cat. If someone visits the cat then the cat visits the dog. If the cat is big then the cat visits the dog.
The cat is big.
("cat" "is" "big" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
If someone visits the cat then the cat does not eat the dog.
((("someone" "visits" "cat" "+")) -> ("cat" "eats" "dog" "-"))
If someone is green then they need the dog.
((("someone" "is" "green" "+")) -> ("someone" "needs" "dog" "+"))
If someone visits the dog then the dog visits the cat.
((("someone" "visits" "dog" "+")) -> ("dog" "visits" "cat" "+"))
If someone needs the dog then the dog eats the cat.
((("someone" "needs" "dog" "+")) -> ("dog" "eats" "cat" "+"))
If someone visits the cat then the cat visits the dog.
((("someone" "visits" "cat" "+")) -> ("cat" "visits" "dog" "+"))
If the cat is big then the cat visits the dog.
((("cat" "is" "big" "+")) -> ("cat" "visits" "dog" "+"))
The cat is big.
True
1
proof
[(triple1)]
("cat" "is" "big" "+")
triple1
The dog does not need the cat.
False
1
inv-proof
[(triple2)]
("dog" "needs" "cat" "-")
triple2
The cat visits the dog.
True
2
proof
[(((triple1) -> rule6))]
("cat" "visits" "dog" "+")
((triple1) -> (rule6 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat does not visit the dog.
False
2
inv-proof
[(((triple1) -> rule6))]
("cat" "visits" "dog" "-")
((triple1) -> (rule6 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The dog visits the cat.
True
3
proof
[(((((triple1) -> rule6)) -> rule3))]
("dog" "visits" "cat" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The dog does not visit the cat.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule3))]
("dog" "visits" "cat" "-")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat does not eat the dog.
True
4
proof
[(((((((triple1) -> rule6)) -> rule3)) -> rule1))]
("cat" "eats" "dog" "-")
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat does not eat the dog.
("cat" "eats" "dog" "-")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat eats the dog.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule3)) -> rule1))]
("cat" "eats" "dog" "+")
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat does not eat the dog.
("cat" "eats" "dog" "-")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat does not need the dog.
Unknown
inv-rconc
[@1: The cat needs the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "needs" "dog" "-")
The dog eats the cat.
Unknown
rconc
[@2: The dog eats the cat.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("dog" "eats" "cat" "+")
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "dog" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat is big.[(triple1)] The dog needs the cat.[(triple2)] @1: The cat visits the dog.[(((triple1) -> rule6))] @2: The dog visits the cat.[(((((triple1) -> rule6)) -> rule3))] @3: The cat does not eat the dog.[(((((((triple1) -> rule6)) -> rule3)) -> rule1))]
The cat is big.
("cat" "is" "big" "+")
triple1
The dog needs the cat.
("dog" "needs" "cat" "+")
triple2
The cat visits the dog.
("cat" "visits" "dog" "+")
((triple1) -> (rule6 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat does not eat the dog.
("cat" "eats" "dog" "-")
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cat does not eat the dog.
("cat" "eats" "dog" "-")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3