The cat eats the dog. The cat is young. The cat visits the cow. The cow eats the cat. The cow is young. The cow visits the dog. The dog is blue. If the dog is young then the dog visits the cat. If something sees the cow and it is rough then it visits the cow. If something sees the cat then the cat eats the dog. If something eats the cat then it eats the cow. If something visits the dog then the dog eats the cat. If something sees the dog and the dog is rough then the dog sees the cow.
The cat eats the dog.
("cat" "eats" "dog" "+")
The cat is young.
("cat" "is" "young" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow eats the cat.
("cow" "eats" "cat" "+")
The cow is young.
("cow" "is" "young" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog is blue.
("dog" "is" "blue" "+")
If the dog is young then the dog visits the cat.
((("dog" "is" "young" "+")) -> ("dog" "visits" "cat" "+"))
If something sees the cow and it is rough then it visits the cow.
((("something" "sees" "cow" "+") ("something" "is" "rough" "+")) -> ("something" "visits" "cow" "+"))
If something sees the cat then the cat eats the dog.
((("something" "sees" "cat" "+")) -> ("cat" "eats" "dog" "+"))
If something eats the cat then it eats the cow.
((("something" "eats" "cat" "+")) -> ("something" "eats" "cow" "+"))
If something visits the dog then the dog eats the cat.
((("something" "visits" "dog" "+")) -> ("dog" "eats" "cat" "+"))
If something sees the dog and the dog is rough then the dog sees the cow.
((("something" "sees" "dog" "+") ("dog" "is" "rough" "+")) -> ("dog" "sees" "cow" "+"))
The cow eats the cat.
True
1
proof
[(triple4)]
("cow" "eats" "cat" "+")
triple4
The cat does not visit the cow.
False
1
inv-proof
[(triple3)]
("cat" "visits" "cow" "-")
triple3
The cow eats the cow.
True
2
proof
[(((triple4) -> rule4))]
("cow" "eats" "cow" "+")
((triple4) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The dog does not eat the cat.
False
2
inv-proof
[(((triple6) -> rule5))]
("dog" "eats" "cat" "-")
((triple6) -> (rule5 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog eats the cow.
True
3
proof
[(((((triple6) -> rule5)) -> rule4))]
("dog" "eats" "cow" "+")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The dog does not eat the cow.
False
3
inv-proof
[(((((triple6) -> rule5)) -> rule4))]
("dog" "eats" "cow" "-")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The cow does not visit the cow.
Unknown
inv-rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "visits" "cow" "-")
The cat eats the cow.
Unknown
rconc
[@1: The cat eats the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "eats" "cow" "+")
The dog does not see the cow.
Unknown
inv-rconc
[@1: The dog sees the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "sees" "cow" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
@0: The cat eats the dog.[(triple1)] The cat is young.[(triple2)] The cat visits the cow.[(triple3)] The cow eats the cat.[(triple4)] The cow is young.[(triple5)] The cow visits the dog.[(triple6)] The dog is blue.[(triple7)] @1: The cow eats the cow.[(((triple4) -> rule4))] The dog eats the cat.[(((triple6) -> rule5))] @2: The dog eats the cow.[(((((triple6) -> rule5)) -> rule4))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The cat is young.
("cat" "is" "young" "+")
triple2
The cat visits the cow.
("cat" "visits" "cow" "+")
triple3
The cow eats the cat.
("cow" "eats" "cat" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5
The cow visits the dog.
("cow" "visits" "dog" "+")
triple6
The dog is blue.
("dog" "is" "blue" "+")
triple7
The cow eats the cow.
("cow" "eats" "cow" "+")
((triple4) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
((triple6) -> (rule5 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog eats the cow.
("dog" "eats" "cow" "+")
((((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The dog eats the cow.
("dog" "eats" "cow" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2