The cat does not chase the mouse. The cat is red. The cat sees the cow. The cat sees the dog. The cat sees the mouse. The cow chases the cat. The cow chases the mouse. The cow is green. The cow does not visit the dog. The dog sees the cow. The mouse chases the cat. The mouse is red. The mouse is not rough. The mouse sees the cat. The mouse visits the cow. If something is big and it visits the mouse then the mouse is red. If something visits the dog and it is cold then the dog does not chase the cow. If the dog visits the mouse then the dog sees the cow. If something visits the cat and it visits the mouse then the cat visits the mouse. If something visits the dog then it chases the cat. If something chases the cat and it does not chase the mouse then the mouse visits the cat. If something sees the cat then the cat visits the dog. If something is rough then it is green.
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
The cat is red.
("cat" "is" "red" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The cow is green.
("cow" "is" "green" "+")
The cow does not visit the dog.
("cow" "visits" "dog" "-")
The dog sees the cow.
("dog" "sees" "cow" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If something is big and it visits the mouse then the mouse is red.
((("something" "is" "big" "+") ("something" "visits" "mouse" "+")) -> ("mouse" "is" "red" "+"))
If something visits the dog and it is cold then the dog does not chase the cow.
((("something" "visits" "dog" "+") ("something" "is" "cold" "+")) -> ("dog" "chases" "cow" "-"))
If the dog visits the mouse then the dog sees the cow.
((("dog" "visits" "mouse" "+")) -> ("dog" "sees" "cow" "+"))
If something visits the cat and it visits the mouse then the cat visits the mouse.
((("something" "visits" "cat" "+") ("something" "visits" "mouse" "+")) -> ("cat" "visits" "mouse" "+"))
If something visits the dog then it chases the cat.
((("something" "visits" "dog" "+")) -> ("something" "chases" "cat" "+"))
If something chases the cat and it does not chase the mouse then the mouse visits the cat.
((("something" "chases" "cat" "+") ("something" "chases" "mouse" "~")) -> ("mouse" "visits" "cat" "+"))
If something sees the cat then the cat visits the dog.
((("something" "sees" "cat" "+")) -> ("cat" "visits" "dog" "+"))
If something is rough then it is green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
The cow does not visit the dog.
True
1
proof
[(triple9)]
("cow" "visits" "dog" "-")
triple9
The cat does not see the dog.
False
1
inv-proof
[(triple4)]
("cat" "sees" "dog" "-")
triple4
The cat visits the dog.
True
2
proof
[(((triple14) -> rule7))]
("cat" "visits" "dog" "+")
((triple14) -> (rule7 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat does not visit the dog.
False
2
inv-proof
[(((triple14) -> rule7))]
("cat" "visits" "dog" "-")
((triple14) -> (rule7 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat chases the cat.
True
3
proof
[(((((triple14) -> rule7)) -> rule5))]
("cat" "chases" "cat" "+")
((((triple14) -> (rule7 % int2))) -> (rule5 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat does not chase the cat.
False
3
inv-proof
[(((((triple14) -> rule7)) -> rule5))]
("cat" "chases" "cat" "-")
((((triple14) -> (rule7 % int2))) -> (rule5 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The mouse visits the cat.
True
5
proof
[(((((((triple14) -> rule7)) -> rule5) triple1) -> rule6))]
("mouse" "visits" "cat" "+")
((((((triple14) -> (rule7 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The mouse does not visit the cat.
False
5
inv-proof
[(((((((triple14) -> rule7)) -> rule5) triple1) -> rule6))]
("mouse" "visits" "cat" "-")
((((((triple14) -> (rule7 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The mouse is not green.
Unknown
inv-rconc
[@1: The mouse is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "is" "green" "-")
The cat is green.
Unknown
rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "green" "+")
The cat does not visit the mouse.
Unknown
inv-rconc
[@1: The cat visits the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "visits" "mouse" "-")
The dog is green.
Unknown
rconc
[@1: The dog is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "is" "green" "+")
The mouse does not see the cow.
Unknown
inv-random
[@0: The mouse sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "cow" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The cat does not chase the mouse.[(triple1)] The cat is red.[(triple2)] The cat sees the cow.[(triple3)] The cat sees the dog.[(triple4)] The cat sees the mouse.[(triple5)] The cow chases the cat.[(triple6)] The cow chases the mouse.[(triple7)] The cow does not visit the dog.[(triple9)] The cow is green.[(triple8)] The dog sees the cow.[(triple10)] The mouse chases the cat.[(triple11)] The mouse is not rough.[(triple13)] The mouse is red.[(triple12)] The mouse sees the cat.[(triple14)] The mouse visits the cow.[(triple15)] @1: The cat visits the dog.[(((triple14) -> rule7))] @2: The cat chases the cat.[(((((triple14) -> rule7)) -> rule5))] @3: The mouse visits the cat.[(((((((triple14) -> rule7)) -> rule5) triple1) -> rule6))]
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
triple1
The cat is red.
("cat" "is" "red" "+")
triple2
The cat sees the cow.
("cat" "sees" "cow" "+")
triple3
The cat sees the dog.
("cat" "sees" "dog" "+")
triple4
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple5
The cow chases the cat.
("cow" "chases" "cat" "+")
triple6
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple7
The cow does not visit the dog.
("cow" "visits" "dog" "-")
triple9
The cow is green.
("cow" "is" "green" "+")
triple8
The dog sees the cow.
("dog" "sees" "cow" "+")
triple10
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple11
The mouse is not rough.
("mouse" "is" "rough" "-")
triple13
The mouse is red.
("mouse" "is" "red" "+")
triple12
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple14
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple15
The cat visits the dog.
("cat" "visits" "dog" "+")
((triple14) -> (rule7 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
((((triple14) -> (rule7 % int2))) -> (rule5 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The mouse visits the cat.
("mouse" "visits" "cat" "+")
((((((triple14) -> (rule7 % int3))) -> (rule5 % int2)) triple1) -> (rule6 % int1))
The mouse visits the cat.
("mouse" "visits" "cat" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3