The cow eats the dog. The cow is not rough. The dog likes the cow. If someone eats the cow and they chase the dog then the dog eats the cow. If someone chases the dog then they like the dog. If someone is green then they eat the cow. If someone likes the cow then the cow is green. If the dog is rough and the dog likes the cow then the cow does not eat the dog. If someone eats the dog and they eat the cow then they like the cow.
The cow eats the dog.
("cow" "eats" "dog" "+")
The cow is not rough.
("cow" "is" "rough" "-")
The dog likes the cow.
("dog" "likes" "cow" "+")
If someone eats the cow and they chase the dog then the dog eats the cow.
((("someone" "eats" "cow" "+") ("someone" "chases" "dog" "+")) -> ("dog" "eats" "cow" "+"))
If someone chases the dog then they like the dog.
((("someone" "chases" "dog" "+")) -> ("someone" "likes" "dog" "+"))
If someone is green then they eat the cow.
((("someone" "is" "green" "+")) -> ("someone" "eats" "cow" "+"))
If someone likes the cow then the cow is green.
((("someone" "likes" "cow" "+")) -> ("cow" "is" "green" "+"))
If the dog is rough and the dog likes the cow then the cow does not eat the dog.
((("dog" "is" "rough" "+") ("dog" "likes" "cow" "+")) -> ("cow" "eats" "dog" "-"))
If someone eats the dog and they eat the cow then they like the cow.
((("someone" "eats" "dog" "+") ("someone" "eats" "cow" "+")) -> ("someone" "likes" "cow" "+"))
The cow is not rough.
True
1
proof
[(triple2)]
("cow" "is" "rough" "-")
triple2
The dog does not like the cow.
False
1
inv-proof
[(triple3)]
("dog" "likes" "cow" "-")
triple3
The cow is green.
True
2
proof
[(((triple3) -> rule4))]
("cow" "is" "green" "+")
((triple3) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is not green.
False
2
inv-proof
[(((triple3) -> rule4))]
("cow" "is" "green" "-")
((triple3) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow eats the cow.
True
3
proof
[(((((triple3) -> rule4)) -> rule3))]
("cow" "eats" "cow" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow does not eat the cow.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule3))]
("cow" "eats" "cow" "-")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow likes the cow.
True
5
proof
[(((triple1 ((((triple3) -> rule4)) -> rule3)) -> rule6))]
("cow" "likes" "cow" "+")
((triple1 ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow does not like the cow.
False
5
inv-proof
[(((triple1 ((((triple3) -> rule4)) -> rule3)) -> rule6))]
("cow" "likes" "cow" "-")
((triple1 ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The dog does not like the dog.
Unknown
inv-rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "likes" "dog" "-")
The cow likes the dog.
Unknown
rconc
[@1: The cow likes the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "likes" "dog" "+")
The dog does not eat the cow.
Unknown
inv-rconc
[@1: The dog eats the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "eats" "cow" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The dog chases the cow.
Unknown
random
[@0: The dog chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "cow" "+")
@0: The cow eats the dog.[(triple1)] The cow is not rough.[(triple2)] The dog likes the cow.[(triple3)] @1: The cow is green.[(((triple3) -> rule4))] @2: The cow eats the cow.[(((((triple3) -> rule4)) -> rule3))] @3: The cow likes the cow.[(((triple1 ((((triple3) -> rule4)) -> rule3)) -> rule6))]
The cow eats the dog.
("cow" "eats" "dog" "+")
triple1
The cow is not rough.
("cow" "is" "rough" "-")
triple2
The dog likes the cow.
("dog" "likes" "cow" "+")
triple3
The cow is green.
("cow" "is" "green" "+")
((triple3) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple1 ((((triple3) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow eats the cow.
("cow" "eats" "cow" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3