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