The cow is cold. The cow sees the dog. The cow visits the dog. The dog eats the cow. The dog is blue. The dog is cold. The dog is kind. The dog is not nice. The dog does not see the cow. The dog visits the cow. If someone eats the cow then they visit the dog. If someone visits the cow and the cow is nice then they see the cow. If someone is cold then they visit the cow. If someone visits the cow and they see the dog then the cow sees the dog. If the dog visits the cow and the cow is not kind then the dog sees the cow. If someone is blue and they do not see the dog then they are young.
The cow is cold.
("cow" "is" "cold" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is not nice.
("dog" "is" "nice" "-")
The dog does not see the cow.
("dog" "sees" "cow" "-")
The dog visits the cow.
("dog" "visits" "cow" "+")
If someone eats the cow then they visit the dog.
((("someone" "eats" "cow" "+")) -> ("someone" "visits" "dog" "+"))
If someone visits the cow and the cow is nice then they see the cow.
((("someone" "visits" "cow" "+") ("cow" "is" "nice" "+")) -> ("someone" "sees" "cow" "+"))
If someone is cold then they visit the cow.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "cow" "+"))
If someone visits the cow and they see the dog then the cow sees the dog.
((("someone" "visits" "cow" "+") ("someone" "sees" "dog" "+")) -> ("cow" "sees" "dog" "+"))
If the dog visits the cow and the cow is not kind then the dog sees the cow.
((("dog" "visits" "cow" "+") ("cow" "is" "kind" "~")) -> ("dog" "sees" "cow" "+"))
If someone is blue and they do not see the dog then they are young.
((("someone" "is" "blue" "+") ("someone" "sees" "dog" "~")) -> ("someone" "is" "young" "+"))
The cow is cold.
True
1
proof
[(triple1)]
("cow" "is" "cold" "+")
triple1
The dog is not blue.
False
1
inv-proof
[(triple5)]
("dog" "is" "blue" "-")
triple5
The cow visits the cow.
True
2
proof
[(((triple1) -> rule3))]
("cow" "visits" "cow" "+")
((triple1) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow does not visit the cow.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "visits" "cow" "-")
((triple1) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "young" "-")
The dog is young.
Unknown
rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "young" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The dog eats the dog.
Unknown
random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "+")
@0: The cow is cold.[(triple1)] The cow sees the dog.[(triple2)] The cow visits the dog.[(triple3)] The dog does not see the cow.[(triple9)] The dog eats the cow.[(triple4)] The dog is blue.[(triple5)] The dog is cold.[(triple6)] The dog is kind.[(triple7)] The dog is not nice.[(triple8)] The dog visits the cow.[(triple10 OR ((triple6) -> rule3))] @1: The cow visits the cow.[(((triple1) -> rule3))] The dog visits the dog.[(((triple4) -> rule1))]
The cow is cold.
("cow" "is" "cold" "+")
triple1
The cow sees the dog.
("cow" "sees" "dog" "+")
triple2
The cow visits the dog.
("cow" "visits" "dog" "+")
triple3
The dog does not see the cow.
("dog" "sees" "cow" "-")
triple9
The dog eats the cow.
("dog" "eats" "cow" "+")
triple4
The dog is blue.
("dog" "is" "blue" "+")
triple5
The dog is cold.
("dog" "is" "cold" "+")
triple6
The dog is kind.
("dog" "is" "kind" "+")
triple7
The dog is not nice.
("dog" "is" "nice" "-")
triple8
The dog visits the cow.
("dog" "visits" "cow" "+")
triple10
((triple6) -> (rule3 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple1) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple4) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1