The cow chases the dog. The cow is cold. The cow is kind. The cow is nice. The cow needs the dog. The cow visits the dog. The cow visits the lion. The dog needs the cow. The dog visits the cow. The lion is red. If something visits the cow then it is red.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The lion is red.
("lion" "is" "red" "+")
If something visits the cow then it is red.
((("something" "visits" "cow" "+")) -> ("something" "is" "red" "+"))
The cow is cold.
True
1
proof
[(triple2)]
("cow" "is" "cold" "+")
triple2
The cow does not visit the lion.
False
1
inv-proof
[(triple7)]
("cow" "visits" "lion" "-")
triple7
The dog is red.
True
2
proof
[(((triple9) -> rule1))]
("dog" "is" "red" "+")
((triple9) -> (rule1 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is not red.
False
2
inv-proof
[(((triple9) -> rule1))]
("dog" "is" "red" "-")
((triple9) -> (rule1 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The cow is not red.
Unknown
inv-rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "red" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
The cow does not chase the lion.
Unknown
inv-random
[@0: The cow chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "lion" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The cow chases the dog.[(triple1)] The cow is cold.[(triple2)] The cow is kind.[(triple3)] The cow is nice.[(triple4)] The cow needs the dog.[(triple5)] The cow visits the dog.[(triple6)] The cow visits the lion.[(triple7)] The dog needs the cow.[(triple8)] The dog visits the cow.[(triple9)] The lion is red.[(triple10)] @1: The dog is red.[(((triple9) -> rule1))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow is kind.
("cow" "is" "kind" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow needs the dog.
("cow" "needs" "dog" "+")
triple5
The cow visits the dog.
("cow" "visits" "dog" "+")
triple6
The cow visits the lion.
("cow" "visits" "lion" "+")
triple7
The dog needs the cow.
("dog" "needs" "cow" "+")
triple8
The dog visits the cow.
("dog" "visits" "cow" "+")
triple9
The lion is red.
("lion" "is" "red" "+")
triple10
The dog is red.
("dog" "is" "red" "+")
((triple9) -> (rule1 % int1))
The dog is red.
("dog" "is" "red" "+")
int1