The cat chases the cow. The cat eats the cow. The cat is green. The cat sees the cow. The cow chases the cat. The cow is rough. The cow sees the cat. If something eats the cow and it eats the cat then it is cold. If something sees the cow then it eats the cat.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is green.
("cat" "is" "green" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
If something eats the cow and it eats the cat then it is cold.
((("something" "eats" "cow" "+") ("something" "eats" "cat" "+")) -> ("something" "is" "cold" "+"))
If something sees the cow then it eats the cat.
((("something" "sees" "cow" "+")) -> ("something" "eats" "cat" "+"))
The cat is green.
True
1
proof
[(triple3)]
("cat" "is" "green" "+")
triple3
The cat is not green.
False
1
inv-proof
[(triple3)]
("cat" "is" "green" "-")
triple3
The cat eats the cat.
True
2
proof
[(((triple4) -> rule2))]
("cat" "eats" "cat" "+")
((triple4) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat does not eat the cat.
False
2
inv-proof
[(((triple4) -> rule2))]
("cat" "eats" "cat" "-")
((triple4) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is cold.
True
4
proof
[(((triple2 ((triple4) -> rule2)) -> rule1))]
("cat" "is" "cold" "+")
((triple2 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cat is not cold.
False
4
inv-proof
[(((triple2 ((triple4) -> rule2)) -> rule1))]
("cat" "is" "cold" "-")
((triple2 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2
The cow is not cold.
Unknown
inv-rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "cold" "-")
The cow eats the cat.
Unknown
rconc
[@1: The cow eats the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "eats" "cat" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The cow is big.
Unknown
random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "+")
@0: The cat chases the cow.[(triple1)] The cat eats the cow.[(triple2)] The cat is green.[(triple3)] The cat sees the cow.[(triple4)] The cow chases the cat.[(triple5)] The cow is rough.[(triple6)] The cow sees the cat.[(triple7)] @1: The cat eats the cat.[(((triple4) -> rule2))] @2: The cat is cold.[(((triple2 ((triple4) -> rule2)) -> rule1))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat eats the cow.
("cat" "eats" "cow" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat sees the cow.
("cat" "sees" "cow" "+")
triple4
The cow chases the cat.
("cow" "chases" "cat" "+")
triple5
The cow is rough.
("cow" "is" "rough" "+")
triple6
The cow sees the cat.
("cow" "sees" "cat" "+")
triple7
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple4) -> (rule2 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
((triple2 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
int2