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