The cat chases the cow. The cat chases the mouse. The cat is green. The cat is kind. The cat is nice. The cow is nice. The cow likes the mouse. The cow visits the cat. The mouse chases the cow. The mouse likes the cat. All nice, rough things are cold. If the cat chases the mouse then the mouse is kind. If something likes the cow then it is rough. If something is cold then it chases the cat. If the mouse is kind then the mouse likes the cow. If something likes the cow and the cow likes the cat then the cow is green.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
All nice, rough things are cold.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If the cat chases the mouse then the mouse is kind.
((("cat" "chases" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If something likes the cow then it is rough.
((("something" "likes" "cow" "+")) -> ("something" "is" "rough" "+"))
If something is cold then it chases the cat.
((("something" "is" "cold" "+")) -> ("something" "chases" "cat" "+"))
If the mouse is kind then the mouse likes the cow.
((("mouse" "is" "kind" "+")) -> ("mouse" "likes" "cow" "+"))
If something likes the cow and the cow likes the cat then the cow is green.
((("something" "likes" "cow" "+") ("cow" "likes" "cat" "+")) -> ("cow" "is" "green" "+"))
The cat chases the cow.
True
1
proof
[(triple1)]
("cat" "chases" "cow" "+")
triple1
The mouse does not like the cat.
False
1
inv-proof
[(triple10)]
("mouse" "likes" "cat" "-")
triple10
The mouse is kind.
True
2
proof
[(((triple2) -> rule2))]
("mouse" "is" "kind" "+")
((triple2) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is not kind.
False
2
inv-proof
[(((triple2) -> rule2))]
("mouse" "is" "kind" "-")
((triple2) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse likes the cow.
True
3
proof
[(((((triple2) -> rule2)) -> rule5))]
("mouse" "likes" "cow" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse does not like the cow.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule5))]
("mouse" "likes" "cow" "-")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is rough.
True
4
proof
[(((((((triple2) -> rule2)) -> rule5)) -> rule3))]
("mouse" "is" "rough" "+")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The mouse is not rough.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule5)) -> rule3))]
("mouse" "is" "rough" "-")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3
The cat does not chase the cat.
Unknown
inv-rconc
[@3: The cat chases the cat.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule3 <- FAIL)]]
("cat" "chases" "cat" "-")
The cow is rough.
Unknown
rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "rough" "+")
The cat is not cold.
Unknown
inv-rconc
[@2: The cat is cold.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("cat" "is" "cold" "-")
The mouse is cold.
Unknown
rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "cold" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The cat likes the mouse.
Unknown
random
[@0: The cat likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "mouse" "+")
The cat does not visit the mouse.
Unknown
inv-random
[@0: The cat visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "mouse" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
@0: The cat chases the cow.[(triple1)] The cat chases the mouse.[(triple2)] The cat is green.[(triple3)] The cat is kind.[(triple4)] The cat is nice.[(triple5)] The cow is nice.[(triple6)] The cow likes the mouse.[(triple7)] The cow visits the cat.[(triple8)] The mouse chases the cow.[(triple9)] The mouse likes the cat.[(triple10)] @1: The mouse is kind.[(((triple2) -> rule2))] @2: The mouse likes the cow.[(((((triple2) -> rule2)) -> rule5))] @3: The mouse is rough.[(((((((triple2) -> rule2)) -> rule5)) -> rule3))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat is kind.
("cat" "is" "kind" "+")
triple4
The cat is nice.
("cat" "is" "nice" "+")
triple5
The cow is nice.
("cow" "is" "nice" "+")
triple6
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple7
The cow visits the cat.
("cow" "visits" "cat" "+")
triple8
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple9
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple10
The mouse is kind.
("mouse" "is" "kind" "+")
((triple2) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
((((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int2
The mouse is kind.
("mouse" "is" "kind" "+")
int3