The cow chases the dog. The dog visits the cow. If someone needs the cow then the cow visits the dog. If someone is young then they do not visit the dog. If someone chases the dog then they need the cow. If someone visits the dog then they are blue. If someone needs the dog and they do not visit the cow then they are nice. If someone chases the dog and they do not visit the dog then they are not cold.
The cow chases the dog.
("cow" "chases" "dog" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
If someone needs the cow then the cow visits the dog.
((("someone" "needs" "cow" "+")) -> ("cow" "visits" "dog" "+"))
If someone is young then they do not visit the dog.
((("someone" "is" "young" "+")) -> ("someone" "visits" "dog" "-"))
If someone chases the dog then they need the cow.
((("someone" "chases" "dog" "+")) -> ("someone" "needs" "cow" "+"))
If someone visits the dog then they are blue.
((("someone" "visits" "dog" "+")) -> ("someone" "is" "blue" "+"))
If someone needs the dog and they do not visit the cow then they are nice.
((("someone" "needs" "dog" "+") ("someone" "visits" "cow" "~")) -> ("someone" "is" "nice" "+"))
If someone chases the dog and they do not visit the dog then they are not cold.
((("someone" "chases" "dog" "+") ("someone" "visits" "dog" "~")) -> ("someone" "is" "cold" "-"))
The dog visits the cow.
True
1
proof
[(triple2)]
("dog" "visits" "cow" "+")
triple2
The cow does not chase the dog.
False
1
inv-proof
[(triple1)]
("cow" "chases" "dog" "-")
triple1
The cow needs the cow.
True
2
proof
[(((triple1) -> rule3))]
("cow" "needs" "cow" "+")
((triple1) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not need the cow.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "needs" "cow" "-")
((triple1) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow visits the dog.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("cow" "visits" "dog" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow does not visit the dog.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("cow" "visits" "dog" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is blue.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule4))]
("cow" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
The cow is not blue.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule4))]
("cow" "is" "blue" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "nice" "-")
The dog needs the cow.
Unknown
rconc
[@1: The dog needs the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "needs" "cow" "+")
The dog is not nice.
Unknown
inv-rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "nice" "-")
The dog is blue.
Unknown
rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "blue" "+")
The cow does not need the dog.
Unknown
inv-random
[@0: The cow needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "dog" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cow chases the dog.[(triple1)] The dog visits the cow.[(triple2)] @1: The cow needs the cow.[(((triple1) -> rule3))] @2: The cow visits the dog.[(((((triple1) -> rule3)) -> rule1))] @3: The cow is blue.[(((((((triple1) -> rule3)) -> rule1)) -> rule4))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The dog visits the cow.
("dog" "visits" "cow" "+")
triple2
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple1) -> (rule3 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3