The bear visits the cow. The cat needs the dog. The cow eats the bear. The dog needs the cow. If someone needs the cow then the cow needs the bear. If someone needs the bear then the bear needs the cow. If someone visits the cat then they are big. If the cat needs the dog and the dog is blue then the cat is big. If the cat is green and the cat needs the bear then the bear eats the dog. If someone needs the bear then they need the cow. If someone eats the dog and the dog is cold then they visit the bear. If someone needs the cat and the cat is red then the cat eats the dog.
The bear visits the cow.
("bear" "visits" "cow" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
If someone needs the cow then the cow needs the bear.
((("someone" "needs" "cow" "+")) -> ("cow" "needs" "bear" "+"))
If someone needs the bear then the bear needs the cow.
((("someone" "needs" "bear" "+")) -> ("bear" "needs" "cow" "+"))
If someone visits the cat then they are big.
((("someone" "visits" "cat" "+")) -> ("someone" "is" "big" "+"))
If the cat needs the dog and the dog is blue then the cat is big.
((("cat" "needs" "dog" "+") ("dog" "is" "blue" "+")) -> ("cat" "is" "big" "+"))
If the cat is green and the cat needs the bear then the bear eats the dog.
((("cat" "is" "green" "+") ("cat" "needs" "bear" "+")) -> ("bear" "eats" "dog" "+"))
If someone needs the bear then they need the cow.
((("someone" "needs" "bear" "+")) -> ("someone" "needs" "cow" "+"))
If someone eats the dog and the dog is cold then they visit the bear.
((("someone" "eats" "dog" "+") ("dog" "is" "cold" "+")) -> ("someone" "visits" "bear" "+"))
If someone needs the cat and the cat is red then the cat eats the dog.
((("someone" "needs" "cat" "+") ("cat" "is" "red" "+")) -> ("cat" "eats" "dog" "+"))
The dog needs the cow.
True
1
proof
[(triple4)]
("dog" "needs" "cow" "+")
triple4
The dog does not need the cow.
False
1
inv-proof
[(triple4)]
("dog" "needs" "cow" "-")
triple4
The cow needs the bear.
True
2
proof
[(((triple4) -> rule1))]
("cow" "needs" "bear" "+")
((triple4) -> (rule1 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow does not need the bear.
False
2
inv-proof
[(((triple4) -> rule1))]
("cow" "needs" "bear" "-")
((triple4) -> (rule1 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow needs the cow.
True
3
proof
[(((((triple4) -> rule1)) -> rule6))]
("cow" "needs" "cow" "+")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The cow does not need the cow.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule6))]
("cow" "needs" "cow" "-")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The bear does not eat the dog.
Unknown
inv-rconc
[@1: The bear eats the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "dog" "-")
The dog visits the bear.
Unknown
rconc
[@1: The dog visits the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "visits" "bear" "+")
The cat is not big.
Unknown
inv-rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "big" "-")
The cat is red.
Unknown
random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "+")
The dog does not eat the cat.
Unknown
inv-random
[@0: The dog eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cat" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The bear visits the cow.[(triple1)] The cat needs the dog.[(triple2)] The cow eats the bear.[(triple3)] The dog needs the cow.[(triple4)] @1: The cow needs the bear.[(((triple4) -> rule1))] @2: The bear needs the cow.[(((((triple4) -> rule1)) -> rule2))] The cow needs the cow.[(((((triple4) -> rule1)) -> rule6))]
The bear visits the cow.
("bear" "visits" "cow" "+")
triple1
The cat needs the dog.
("cat" "needs" "dog" "+")
triple2
The cow eats the bear.
("cow" "eats" "bear" "+")
triple3
The dog needs the cow.
("dog" "needs" "cow" "+")
triple4
The cow needs the bear.
("cow" "needs" "bear" "+")
((triple4) -> (rule1 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2