The cow visits the dog. The dog sees the cow. If something is kind then it sees the cow. If something sees the dog then it chases the cow. If something is rough and it visits the dog then the dog chases the cow. If something visits the cow then the cow sees the dog. If something chases the dog and the dog is blue then the dog chases the cow. If the cow sees the dog and the dog visits the cow then the cow is blue. If something chases the dog then the dog is blue. If the dog sees the cow then the dog visits the cow.
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
If something is kind then it sees the cow.
((("something" "is" "kind" "+")) -> ("something" "sees" "cow" "+"))
If something sees the dog then it chases the cow.
((("something" "sees" "dog" "+")) -> ("something" "chases" "cow" "+"))
If something is rough and it visits the dog then the dog chases the cow.
((("something" "is" "rough" "+") ("something" "visits" "dog" "+")) -> ("dog" "chases" "cow" "+"))
If something visits the cow then the cow sees the dog.
((("something" "visits" "cow" "+")) -> ("cow" "sees" "dog" "+"))
If something chases the dog and the dog is blue then the dog chases the cow.
((("something" "chases" "dog" "+") ("dog" "is" "blue" "+")) -> ("dog" "chases" "cow" "+"))
If the cow sees the dog and the dog visits the cow then the cow is blue.
((("cow" "sees" "dog" "+") ("dog" "visits" "cow" "+")) -> ("cow" "is" "blue" "+"))
If something chases the dog then the dog is blue.
((("something" "chases" "dog" "+")) -> ("dog" "is" "blue" "+"))
If the dog sees the cow then the dog visits the cow.
((("dog" "sees" "cow" "+")) -> ("dog" "visits" "cow" "+"))
The cow visits the dog.
True
1
proof
[(triple1)]
("cow" "visits" "dog" "+")
triple1
The cow does not visit the dog.
False
1
inv-proof
[(triple1)]
("cow" "visits" "dog" "-")
triple1
The dog visits the cow.
True
2
proof
[(((triple2) -> rule8))]
("dog" "visits" "cow" "+")
((triple2) -> (rule8 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The dog does not visit the cow.
False
2
inv-proof
[(((triple2) -> rule8))]
("dog" "visits" "cow" "-")
((triple2) -> (rule8 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The cow does not see the cow.
Unknown
inv-rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "cow" "-")
The dog is blue.
Unknown
rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "blue" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The cow visits the dog.[(triple1)] The dog sees the cow.[(triple2)] @1: The dog visits the cow.[(((triple2) -> rule8))] @2: The cow sees the dog.[(((((triple2) -> rule8)) -> rule4))] @3: The cow chases the cow.[(((((((triple2) -> rule8)) -> rule4)) -> rule2))] The cow is blue.[(((((((triple2) -> rule8)) -> rule4) ((triple2) -> rule8)) -> rule6))]
The cow visits the dog.
("cow" "visits" "dog" "+")
triple1
The dog sees the cow.
("dog" "sees" "cow" "+")
triple2
The dog visits the cow.
("dog" "visits" "cow" "+")
((triple2) -> (rule8 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The dog visits the cow.
("dog" "visits" "cow" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
((((((triple2) -> (rule8 % int3))) -> (rule4 % int2)) ((triple2) -> (rule8 % int3))) -> (rule6 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The dog visits the cow.
("dog" "visits" "cow" "+")
int3