The cat likes the cow. The cow is green. The cow does not see the cat. If something likes the cat and the cat does not see the cow then it sees the cat. If the cat chases the cow and the cat sees the cow then the cat does not like the cow. If something chases the cat then the cat likes the cow. If something likes the cat then it chases the cow. If the cow is green then the cow is cold. If something is cold then it likes the cat.
The cat likes the cow.
("cat" "likes" "cow" "+")
The cow is green.
("cow" "is" "green" "+")
The cow does not see the cat.
("cow" "sees" "cat" "-")
If something likes the cat and the cat does not see the cow then it sees the cat.
((("something" "likes" "cat" "+") ("cat" "sees" "cow" "~")) -> ("something" "sees" "cat" "+"))
If the cat chases the cow and the cat sees the cow then the cat does not like the cow.
((("cat" "chases" "cow" "+") ("cat" "sees" "cow" "+")) -> ("cat" "likes" "cow" "-"))
If something chases the cat then the cat likes the cow.
((("something" "chases" "cat" "+")) -> ("cat" "likes" "cow" "+"))
If something likes the cat then it chases the cow.
((("something" "likes" "cat" "+")) -> ("something" "chases" "cow" "+"))
If the cow is green then the cow is cold.
((("cow" "is" "green" "+")) -> ("cow" "is" "cold" "+"))
If something is cold then it likes the cat.
((("something" "is" "cold" "+")) -> ("something" "likes" "cat" "+"))
The cow is green.
True
1
proof
[(triple2)]
("cow" "is" "green" "+")
triple2
The cat does not like the cow.
False
1
inv-proof
[(triple1)]
("cat" "likes" "cow" "-")
triple1
The cow is cold.
True
2
proof
[(((triple2) -> rule5))]
("cow" "is" "cold" "+")
((triple2) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is not cold.
False
2
inv-proof
[(((triple2) -> rule5))]
("cow" "is" "cold" "-")
((triple2) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow likes the cat.
True
3
proof
[(((((triple2) -> rule5)) -> rule6))]
("cow" "likes" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow does not like the cat.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule6))]
("cow" "likes" "cat" "-")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow chases the cow.
True
4
proof
[(((((((triple2) -> rule5)) -> rule6)) -> rule4))]
("cow" "chases" "cow" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow does not chase the cow.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule6)) -> rule4))]
("cow" "chases" "cow" "-")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "cat" "-")
The cat chases the cow.
Unknown
rconc
[@2: The cat chases the cow.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("cat" "chases" "cow" "+")
The cat does not like the cat.
Unknown
inv-rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "likes" "cat" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
The cat is not cold.
Unknown
inv-random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat likes the cow.[(triple1)] The cow does not see the cat.[(triple3)] The cow is green.[(triple2)] @1: The cow is cold.[(((triple2) -> rule5))] @2: The cow likes the cat.[(((((triple2) -> rule5)) -> rule6))] @3: The cow chases the cow.[(((((((triple2) -> rule5)) -> rule6)) -> rule4))]
The cat likes the cow.
("cat" "likes" "cow" "+")
triple1
The cow does not see the cat.
("cow" "sees" "cat" "-")
triple3
The cow is green.
("cow" "is" "green" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
((triple2) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
((((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3