The cat does not chase the mouse. The cow chases the cat. The mouse does not see the cat. If something is blue then it sees the cow. If something chases the cat then it is blue. If something chases the cow then the cow is big. If something chases the cat and the cat is red then it does not see the cat. If something visits the cow then it visits the mouse. If something chases the cat then the cat does not chase the cow. If something chases the cat and the cat visits the cow then the cat is cold. If the cow chases the cat and the cat does not chase the cow then the cow does not visit the cat.
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
The cow chases the cat.
("cow" "chases" "cat" "+")
The mouse does not see the cat.
("mouse" "sees" "cat" "-")
If something is blue then it sees the cow.
((("something" "is" "blue" "+")) -> ("something" "sees" "cow" "+"))
If something chases the cat then it is blue.
((("something" "chases" "cat" "+")) -> ("something" "is" "blue" "+"))
If something chases the cow then the cow is big.
((("something" "chases" "cow" "+")) -> ("cow" "is" "big" "+"))
If something chases the cat and the cat is red then it does not see the cat.
((("something" "chases" "cat" "+") ("cat" "is" "red" "+")) -> ("something" "sees" "cat" "-"))
If something visits the cow then it visits the mouse.
((("something" "visits" "cow" "+")) -> ("something" "visits" "mouse" "+"))
If something chases the cat then the cat does not chase the cow.
((("something" "chases" "cat" "+")) -> ("cat" "chases" "cow" "-"))
If something chases the cat and the cat visits the cow then the cat is cold.
((("something" "chases" "cat" "+") ("cat" "visits" "cow" "+")) -> ("cat" "is" "cold" "+"))
If the cow chases the cat and the cat does not chase the cow then the cow does not visit the cat.
((("cow" "chases" "cat" "+") ("cat" "chases" "cow" "~")) -> ("cow" "visits" "cat" "-"))
The cat does not chase the mouse.
True
1
proof
[(triple1)]
("cat" "chases" "mouse" "-")
triple1
The mouse sees the cat.
False
1
inv-proof
[(triple3)]
("mouse" "sees" "cat" "+")
triple3
The cat does not chase the cow.
True
2
proof
[(((triple2) -> rule6))]
("cat" "chases" "cow" "-")
((triple2) -> (rule6 % int1))
The cat does not chase the cow.
("cat" "chases" "cow" "-")
int1
The cat chases the cow.
False
2
inv-proof
[(((triple2) -> rule6))]
("cat" "chases" "cow" "+")
((triple2) -> (rule6 % int1))
The cat does not chase the cow.
("cat" "chases" "cow" "-")
int1
The cow does not visit the cat.
True
4
proof
[(((triple2 ((triple2) -> rule6)) -> rule8))]
("cow" "visits" "cat" "-")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule8 % int1))
The cow does not visit the cat.
("cow" "visits" "cat" "-")
int1
The cat does not chase the cow.
("cat" "chases" "cow" "-")
int2
The cow does not see the cow.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("cow" "sees" "cow" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The cow does not visit the mouse.
Unknown
inv-rconc
[@1: The cow visits the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "visits" "mouse" "-")
The mouse sees the cow.
Unknown
rconc
[@2: The mouse sees the cow.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("mouse" "sees" "cow" "+")
The cat does not visit the mouse.
Unknown
inv-rconc
[@1: The cat visits the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "visits" "mouse" "-")
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 mouse.
Unknown
inv-random
[@0: The cow chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "mouse" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat does not chase the mouse.[(triple1)] The cow chases the cat.[(triple2)] The mouse does not see the cat.[(triple3)] @1: The cat does not chase the cow.[(((triple2) -> rule6))] The cow is blue.[(((triple2) -> rule2))] @2: The cow does not visit the cat.[(((triple2 ((triple2) -> rule6)) -> rule8))] The cow sees the cow.[(((((triple2) -> rule2)) -> rule1))]
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
triple1
The cow chases the cat.
("cow" "chases" "cat" "+")
triple2
The mouse does not see the cat.
("mouse" "sees" "cat" "-")
triple3
The cat does not chase the cow.
("cat" "chases" "cow" "-")
((triple2) -> (rule6 % int1))
The cat does not chase the cow.
("cat" "chases" "cow" "-")
int1
The cow is blue.
("cow" "is" "blue" "+")
((triple2) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow does not visit the cat.
("cow" "visits" "cat" "-")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule8 % int1))
The cow does not visit the cat.
("cow" "visits" "cat" "-")
int1
The cat does not chase the cow.
("cat" "chases" "cow" "-")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2