The dog is big. The dog is rough. The dog visits the mouse. The dog visits the rabbit. The lion is young. The mouse is big. The rabbit sees the mouse. If someone sees the mouse then the mouse chases the rabbit. If someone visits the rabbit then the rabbit visits the lion. If someone visits the lion then they chase the rabbit. If the dog is big and the dog visits the rabbit then the dog sees the rabbit. If someone sees the lion and they see the rabbit then the rabbit chases the mouse. If the dog visits the lion and the dog visits the mouse then the dog is red.
The dog is big.
("dog" "is" "big" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The lion is young.
("lion" "is" "young" "+")
The mouse is big.
("mouse" "is" "big" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If someone sees the mouse then the mouse chases the rabbit.
((("someone" "sees" "mouse" "+")) -> ("mouse" "chases" "rabbit" "+"))
If someone visits the rabbit then the rabbit visits the lion.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "visits" "lion" "+"))
If someone visits the lion then they chase the rabbit.
((("someone" "visits" "lion" "+")) -> ("someone" "chases" "rabbit" "+"))
If the dog is big and the dog visits the rabbit then the dog sees the rabbit.
((("dog" "is" "big" "+") ("dog" "visits" "rabbit" "+")) -> ("dog" "sees" "rabbit" "+"))
If someone sees the lion and they see the rabbit then the rabbit chases the mouse.
((("someone" "sees" "lion" "+") ("someone" "sees" "rabbit" "+")) -> ("rabbit" "chases" "mouse" "+"))
If the dog visits the lion and the dog visits the mouse then the dog is red.
((("dog" "visits" "lion" "+") ("dog" "visits" "mouse" "+")) -> ("dog" "is" "red" "+"))
The dog visits the rabbit.
True
1
proof
[(triple4)]
("dog" "visits" "rabbit" "+")
triple4
The dog is not rough.
False
1
inv-proof
[(triple2)]
("dog" "is" "rough" "-")
triple2
The dog sees the rabbit.
True
3
proof
[(((triple1 triple4) -> rule4))]
("dog" "sees" "rabbit" "+")
((triple1 triple4) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The mouse does not chase the rabbit.
False
2
inv-proof
[(((triple7) -> rule1))]
("mouse" "chases" "rabbit" "-")
((triple7) -> (rule1 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The dog does not chase the rabbit.
Unknown
inv-rconc
[@1: The dog chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "rabbit" "-")
The dog is red.
Unknown
rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "red" "+")
The lion does not see the rabbit.
Unknown
inv-random
[@0: The lion sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "rabbit" "-")
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 big.[(triple1)] The dog is rough.[(triple2)] The dog visits the mouse.[(triple3)] The dog visits the rabbit.[(triple4)] The lion is young.[(triple5)] The mouse is big.[(triple6)] The rabbit sees the mouse.[(triple7)] @1: The dog sees the rabbit.[(((triple1 triple4) -> rule4))] The mouse chases the rabbit.[(((triple7) -> rule1))] The rabbit visits the lion.[(((triple4) -> rule2))] @2: The rabbit chases the rabbit.[(((((triple4) -> rule2)) -> rule3))]
The dog is big.
("dog" "is" "big" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple3
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
The mouse is big.
("mouse" "is" "big" "+")
triple6
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple7
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
((triple1 triple4) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
((triple7) -> (rule1 % int1))
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
int1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
((triple4) -> (rule2 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int2