The dog sees the mouse. The mouse chases the dog. The mouse is round. If the mouse is big and the mouse visits the dog then the mouse sees the dog. If something is rough then it visits the dog. If something sees the mouse and it visits the dog then the mouse chases the dog. If something chases the dog then it is rough. If something chases the mouse then it is cold. If something sees the mouse then it is round. If something visits the dog and it sees the mouse then the mouse sees the dog. If something is cold and it visits the mouse then it sees the dog.
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse is round.
("mouse" "is" "round" "+")
If the mouse is big and the mouse visits the dog then the mouse sees the dog.
((("mouse" "is" "big" "+") ("mouse" "visits" "dog" "+")) -> ("mouse" "sees" "dog" "+"))
If something is rough then it visits the dog.
((("something" "is" "rough" "+")) -> ("something" "visits" "dog" "+"))
If something sees the mouse and it visits the dog then the mouse chases the dog.
((("something" "sees" "mouse" "+") ("something" "visits" "dog" "+")) -> ("mouse" "chases" "dog" "+"))
If something chases the dog then it is rough.
((("something" "chases" "dog" "+")) -> ("something" "is" "rough" "+"))
If something chases the mouse then it is cold.
((("something" "chases" "mouse" "+")) -> ("something" "is" "cold" "+"))
If something sees the mouse then it is round.
((("something" "sees" "mouse" "+")) -> ("something" "is" "round" "+"))
If something visits the dog and it sees the mouse then the mouse sees the dog.
((("something" "visits" "dog" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "sees" "dog" "+"))
If something is cold and it visits the mouse then it sees the dog.
((("something" "is" "cold" "+") ("something" "visits" "mouse" "+")) -> ("something" "sees" "dog" "+"))
The mouse is round.
True
1
proof
[(triple3)]
("mouse" "is" "round" "+")
triple3
The mouse does not chase the dog.
False
1
inv-proof
[(triple2)]
("mouse" "chases" "dog" "-")
triple2
The dog is round.
True
2
proof
[(((triple1) -> rule6))]
("dog" "is" "round" "+")
((triple1) -> (rule6 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The mouse is not rough.
False
2
inv-proof
[(((triple2) -> rule4))]
("mouse" "is" "rough" "-")
((triple2) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse visits the dog.
True
3
proof
[(((((triple2) -> rule4)) -> rule2))]
("mouse" "visits" "dog" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse does not visit the dog.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule2))]
("mouse" "visits" "dog" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "sees" "dog" "-")
The dog is cold.
Unknown
rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "cold" "+")
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "cold" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The mouse is not big.
Unknown
inv-random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "-")
The dog visits the mouse.
Unknown
random
[@0: The dog visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "mouse" "+")
@0: The dog sees the mouse.[(triple1)] The mouse chases the dog.[(triple2)] The mouse is round.[(triple3)] @1: The dog is round.[(((triple1) -> rule6))] The mouse is rough.[(((triple2) -> rule4))] @2: The mouse visits the dog.[(((((triple2) -> rule4)) -> rule2))]
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple2
The mouse is round.
("mouse" "is" "round" "+")
triple3
The dog is round.
("dog" "is" "round" "+")
((triple1) -> (rule6 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((triple2) -> (rule4 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2