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