The cow needs the dog. The dog is rough. If something visits the dog then it is green. If something visits the cow and it visits the dog then the dog is nice. If something is green and it visits the dog then the dog is round. If something chases the dog then it needs the cow. If something is rough then it visits the dog. If something chases the cow then the cow chases the dog.
The cow needs the dog.
("cow" "needs" "dog" "+")
The dog is rough.
("dog" "is" "rough" "+")
If something visits the dog then it is green.
((("something" "visits" "dog" "+")) -> ("something" "is" "green" "+"))
If something visits the cow and it visits the dog then the dog is nice.
((("something" "visits" "cow" "+") ("something" "visits" "dog" "+")) -> ("dog" "is" "nice" "+"))
If something is green and it visits the dog then the dog is round.
((("something" "is" "green" "+") ("something" "visits" "dog" "+")) -> ("dog" "is" "round" "+"))
If something chases the dog then it needs the cow.
((("something" "chases" "dog" "+")) -> ("something" "needs" "cow" "+"))
If something is rough then it visits the dog.
((("something" "is" "rough" "+")) -> ("something" "visits" "dog" "+"))
If something chases the cow then the cow chases the dog.
((("something" "chases" "cow" "+")) -> ("cow" "chases" "dog" "+"))
The dog is rough.
True
1
proof
[(triple2)]
("dog" "is" "rough" "+")
triple2
The cow does not need the dog.
False
1
inv-proof
[(triple1)]
("cow" "needs" "dog" "-")
triple1
The dog visits the dog.
True
2
proof
[(((triple2) -> rule5))]
("dog" "visits" "dog" "+")
((triple2) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog does not visit the dog.
False
2
inv-proof
[(((triple2) -> rule5))]
("dog" "visits" "dog" "-")
((triple2) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is green.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("dog" "is" "green" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog is not green.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("dog" "is" "green" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog is round.
True
6
proof
[(((((((triple2) -> rule5)) -> rule1) ((triple2) -> rule5)) -> rule3))]
("dog" "is" "round" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2)) ((triple2) -> (rule5 % int3))) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The dog is not round.
False
6
inv-proof
[(((((((triple2) -> rule5)) -> rule1) ((triple2) -> rule5)) -> rule3))]
("dog" "is" "round" "-")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2)) ((triple2) -> (rule5 % int3))) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3
The cow does not need the cow.
Unknown
inv-rconc
[@2: The cow needs the cow.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("cow" "needs" "cow" "-")
The dog is nice.
Unknown
rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "nice" "+")
The cow does not chase the dog.
Unknown
inv-rconc
[@1: The cow chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "chases" "dog" "-")
The dog needs the cow.
Unknown
rconc
[@1: The dog needs the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "needs" "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 cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The dog does not chase the cow.
Unknown
inv-random
[@0: The dog chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "cow" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cow needs the dog.[(triple1)] The dog is rough.[(triple2)] @1: The dog visits the dog.[(((triple2) -> rule5))] @2: The dog is green.[(((((triple2) -> rule5)) -> rule1))] @3: The dog is round.[(((((((triple2) -> rule5)) -> rule1) ((triple2) -> rule5)) -> rule3))]
The cow needs the dog.
("cow" "needs" "dog" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple2) -> (rule5 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is green.
("dog" "is" "green" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog is round.
("dog" "is" "round" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2)) ((triple2) -> (rule5 % int3))) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
int3