The dog chases the lion. The lion likes the mouse. The lion visits the mouse. The mouse chases the dog. The mouse chases the lion. The mouse is kind. The mouse likes the lion. The mouse visits the squirrel. The squirrel chases the lion. The squirrel likes the dog. If someone visits the squirrel then the squirrel visits the lion. If someone likes the dog then the dog visits the squirrel. If the mouse is kind and the mouse visits the lion then the mouse chases the squirrel. If someone visits the dog then the dog chases the mouse. If someone chases the squirrel then the squirrel visits the dog. If someone visits the lion then they like the lion.
The dog chases the lion.
("dog" "chases" "lion" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
If someone visits the squirrel then the squirrel visits the lion.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "visits" "lion" "+"))
If someone likes the dog then the dog visits the squirrel.
((("someone" "likes" "dog" "+")) -> ("dog" "visits" "squirrel" "+"))
If the mouse is kind and the mouse visits the lion then the mouse chases the squirrel.
((("mouse" "is" "kind" "+") ("mouse" "visits" "lion" "+")) -> ("mouse" "chases" "squirrel" "+"))
If someone visits the dog then the dog chases the mouse.
((("someone" "visits" "dog" "+")) -> ("dog" "chases" "mouse" "+"))
If someone chases the squirrel then the squirrel visits the dog.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "visits" "dog" "+"))
If someone visits the lion then they like the lion.
((("someone" "visits" "lion" "+")) -> ("someone" "likes" "lion" "+"))
The squirrel chases the lion.
True
1
proof
[(triple9)]
("squirrel" "chases" "lion" "+")
triple9
The mouse does not chase the dog.
False
1
inv-proof
[(triple4)]
("mouse" "chases" "dog" "-")
triple4
The squirrel visits the lion.
True
2
proof
[(((triple8) -> rule1) OR ((((triple10) -> rule2)) -> rule1))]
("squirrel" "visits" "lion" "+")
((triple8) -> (rule1 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
The dog does not visit the squirrel.
False
2
inv-proof
[(((triple10) -> rule2))]
("dog" "visits" "squirrel" "-")
((triple10) -> (rule2 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The squirrel likes the lion.
True
3
proof
[(((((triple8) -> rule1)) -> rule6) OR ((((((triple10) -> rule2)) -> rule1)) -> rule6))]
("squirrel" "likes" "lion" "+")
((((triple8) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
((((((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int3
The squirrel does not like the lion.
False
3
inv-proof
[(((((triple8) -> rule1)) -> rule6) OR ((((((triple10) -> rule2)) -> rule1)) -> rule6))]
("squirrel" "likes" "lion" "-")
((((triple8) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
((((((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int3
The squirrel does not visit the dog.
Unknown
inv-rconc
[@2: The squirrel visits the dog.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("squirrel" "visits" "dog" "-")
The dog chases the mouse.
Unknown
rconc
[@3: The dog chases the mouse.[CWA. Example of deepest failure = (rule4 <- rule5 <- rule3 <- FAIL)]]
("dog" "chases" "mouse" "+")
The dog does not like the lion.
Unknown
inv-rconc
[@1: The dog likes the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "likes" "lion" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The lion does not visit the squirrel.
Unknown
inv-random
[@0: The lion visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "squirrel" "-")
The mouse is red.
Unknown
random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "+")
@0: The dog chases the lion.[(triple1)] The lion likes the mouse.[(triple2)] The lion visits the mouse.[(triple3)] The mouse chases the dog.[(triple4)] The mouse chases the lion.[(triple5)] The mouse is kind.[(triple6)] The mouse likes the lion.[(triple7)] The mouse visits the squirrel.[(triple8)] The squirrel chases the lion.[(triple9)] The squirrel likes the dog.[(triple10)] @1: The dog visits the squirrel.[(((triple10) -> rule2))] The squirrel visits the lion.[(((triple8) -> rule1) OR ((((triple10) -> rule2)) -> rule1))] @2: The squirrel likes the lion.[(((((triple8) -> rule1)) -> rule6) OR ((((((triple10) -> rule2)) -> rule1)) -> rule6))]
The dog chases the lion.
("dog" "chases" "lion" "+")
triple1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple2
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple3
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple4
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple5
The mouse is kind.
("mouse" "is" "kind" "+")
triple6
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple7
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple8
The squirrel chases the lion.
("squirrel" "chases" "lion" "+")
triple9
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple10
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
((triple10) -> (rule2 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
((triple8) -> (rule1 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
((((triple8) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
((((((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int3