The cow chases the dog. The cow is kind. The cow is nice. The cow is red. The cow needs the dog. The dog chases the cow. The dog eats the cow. If something is nice and it needs the cow then the cow is round. If something chases the cow and it is red then the cow eats the dog. If something is kind and it eats the cow then it needs the dog. If something eats the dog then the dog needs the cow. If something is round then it eats the dog. If something needs the dog then the dog is red.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
If something is nice and it needs the cow then the cow is round.
((("something" "is" "nice" "+") ("something" "needs" "cow" "+")) -> ("cow" "is" "round" "+"))
If something chases the cow and it is red then the cow eats the dog.
((("something" "chases" "cow" "+") ("something" "is" "red" "+")) -> ("cow" "eats" "dog" "+"))
If something is kind and it eats the cow then it needs the dog.
((("something" "is" "kind" "+") ("something" "eats" "cow" "+")) -> ("something" "needs" "dog" "+"))
If something eats the dog then the dog needs the cow.
((("something" "eats" "dog" "+")) -> ("dog" "needs" "cow" "+"))
If something is round then it eats the dog.
((("something" "is" "round" "+")) -> ("something" "eats" "dog" "+"))
If something needs the dog then the dog is red.
((("something" "needs" "dog" "+")) -> ("dog" "is" "red" "+"))
The dog eats the cow.
True
1
proof
[(triple7)]
("dog" "eats" "cow" "+")
triple7
The cow does not need the dog.
False
1
inv-proof
[(triple5)]
("cow" "needs" "dog" "-")
triple5
The dog is red.
True
2
proof
[(((triple5) -> rule6))]
("dog" "is" "red" "+")
((triple5) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is not red.
False
2
inv-proof
[(((triple5) -> rule6))]
("dog" "is" "red" "-")
((triple5) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The cow eats the dog.
True
4
proof
[(((triple6 ((triple5) -> rule6)) -> rule2))]
("cow" "eats" "dog" "+")
((triple6 ((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The cow does not eat the dog.
False
4
inv-proof
[(((triple6 ((triple5) -> rule6)) -> rule2))]
("cow" "eats" "dog" "-")
((triple6 ((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog needs the cow.
True
5
proof
[(((((triple6 ((triple5) -> rule6)) -> rule2)) -> rule4))]
("dog" "needs" "cow" "+")
((((triple6 ((triple5) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The dog does not need the cow.
False
5
inv-proof
[(((((triple6 ((triple5) -> rule6)) -> rule2)) -> rule4))]
("dog" "needs" "cow" "-")
((((triple6 ((triple5) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "needs" "dog" "-")
The cow is round.
Unknown
rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "round" "+")
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "eats" "dog" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The dog does not chase the dog.
Unknown
inv-random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
@0: The cow chases the dog.[(triple1)] The cow is kind.[(triple2)] The cow is nice.[(triple3)] The cow is red.[(triple4)] The cow needs the dog.[(triple5)] The dog chases the cow.[(triple6)] The dog eats the cow.[(triple7)] @1: The dog is red.[(((triple5) -> rule6))] @2: The cow eats the dog.[(((triple6 ((triple5) -> rule6)) -> rule2))] @3: The dog needs the cow.[(((((triple6 ((triple5) -> rule6)) -> rule2)) -> rule4))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The cow is kind.
("cow" "is" "kind" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow needs the dog.
("cow" "needs" "dog" "+")
triple5
The dog chases the cow.
("dog" "chases" "cow" "+")
triple6
The dog eats the cow.
("dog" "eats" "cow" "+")
triple7
The dog is red.
("dog" "is" "red" "+")
((triple5) -> (rule6 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
((triple6 ((triple5) -> (rule6 % int2))) -> (rule2 % int1))
The cow eats the dog.
("cow" "eats" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog needs the cow.
("dog" "needs" "cow" "+")
((((triple6 ((triple5) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog needs the cow.
("dog" "needs" "cow" "+")
int1
The cow eats the dog.
("cow" "eats" "dog" "+")
int2
The dog is red.
("dog" "is" "red" "+")
int3