The dog likes the lion. The dog visits the lion. The dog visits the mouse. The lion is rough. The lion likes the mouse. The lion needs the dog. The lion visits the dog. The lion visits the mouse. The mouse is green. The mouse is rough. The mouse needs the lion. The mouse visits the dog. If the mouse visits the dog and the dog needs the lion then the mouse is cold. If something needs the mouse then the mouse needs the dog. If something visits the mouse and the mouse visits the dog then the dog needs the lion. If something visits the dog then it likes the mouse. If something is cold then it visits the lion. If something is green and it needs the dog then it visits the mouse.
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If the mouse visits the dog and the dog needs the lion then the mouse is cold.
((("mouse" "visits" "dog" "+") ("dog" "needs" "lion" "+")) -> ("mouse" "is" "cold" "+"))
If something needs the mouse then the mouse needs the dog.
((("something" "needs" "mouse" "+")) -> ("mouse" "needs" "dog" "+"))
If something visits the mouse and the mouse visits the dog then the dog needs the lion.
((("something" "visits" "mouse" "+") ("mouse" "visits" "dog" "+")) -> ("dog" "needs" "lion" "+"))
If something visits the dog then it likes the mouse.
((("something" "visits" "dog" "+")) -> ("something" "likes" "mouse" "+"))
If something is cold then it visits the lion.
((("something" "is" "cold" "+")) -> ("something" "visits" "lion" "+"))
If something is green and it needs the dog then it visits the mouse.
((("something" "is" "green" "+") ("something" "needs" "dog" "+")) -> ("something" "visits" "mouse" "+"))
The mouse needs the lion.
True
1
proof
[(triple11)]
("mouse" "needs" "lion" "+")
triple11
The lion is not rough.
False
1
inv-proof
[(triple4)]
("lion" "is" "rough" "-")
triple4
The mouse likes the mouse.
True
2
proof
[(((triple12) -> rule4))]
("mouse" "likes" "mouse" "+")
((triple12) -> (rule4 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not like the mouse.
False
2
inv-proof
[(((triple12) -> rule4))]
("mouse" "likes" "mouse" "-")
((triple12) -> (rule4 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is cold.
True
5
proof
[(((triple12 ((triple3 triple12) -> rule3)) -> rule1) OR ((triple12 ((triple8 triple12) -> rule3)) -> rule1))]
("mouse" "is" "cold" "+")
((triple12 ((triple3 triple12) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
((triple12 ((triple8 triple12) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The mouse is not cold.
False
5
inv-proof
[(((triple12 ((triple3 triple12) -> rule3)) -> rule1) OR ((triple12 ((triple8 triple12) -> rule3)) -> rule1))]
("mouse" "is" "cold" "-")
((triple12 ((triple3 triple12) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
((triple12 ((triple8 triple12) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The mouse visits the lion.
True
6
proof
[(((((triple12 ((triple3 triple12) -> rule3)) -> rule1)) -> rule5) OR ((((triple12 ((triple8 triple12) -> rule3)) -> rule1)) -> rule5))]
("mouse" "visits" "lion" "+")
((((triple12 ((triple3 triple12) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The dog needs the lion.
("dog" "needs" "lion" "+")
int3
((((triple12 ((triple8 triple12) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The dog needs the lion.
("dog" "needs" "lion" "+")
int3
The mouse does not visit the lion.
False
6
inv-proof
[(((((triple12 ((triple3 triple12) -> rule3)) -> rule1)) -> rule5) OR ((((triple12 ((triple8 triple12) -> rule3)) -> rule1)) -> rule5))]
("mouse" "visits" "lion" "-")
((((triple12 ((triple3 triple12) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The dog needs the lion.
("dog" "needs" "lion" "+")
int3
((((triple12 ((triple8 triple12) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The dog needs the lion.
("dog" "needs" "lion" "+")
int3
The mouse does not visit the mouse.
Unknown
inv-rconc
[@2: The mouse visits the mouse.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The dog likes the mouse.
Unknown
rconc
[@1: The dog likes the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "likes" "mouse" "+")
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "visits" "lion" "-")
The mouse needs the dog.
Unknown
rconc
[@1: The mouse needs the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "dog" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The lion needs the mouse.
Unknown
random
[@0: The lion needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "mouse" "+")
@0: The dog likes the lion.[(triple1)] The dog visits the lion.[(triple2)] The dog visits the mouse.[(triple3)] The lion is rough.[(triple4)] The lion likes the mouse.[(triple5 OR ((triple7) -> rule4))] The lion needs the dog.[(triple6)] The lion visits the dog.[(triple7)] The lion visits the mouse.[(triple8)] The mouse is green.[(triple9)] The mouse is rough.[(triple10)] The mouse needs the lion.[(triple11)] The mouse visits the dog.[(triple12)] @1: The dog needs the lion.[(((triple3 triple12) -> rule3) OR ((triple8 triple12) -> rule3))] The mouse likes the mouse.[(((triple12) -> rule4))] @2: The mouse is cold.[(((triple12 ((triple3 triple12) -> rule3)) -> rule1) OR ((triple12 ((triple8 triple12) -> rule3)) -> rule1))] @3: The mouse visits the lion.[(((((triple12 ((triple3 triple12) -> rule3)) -> rule1)) -> rule5) OR ((((triple12 ((triple8 triple12) -> rule3)) -> rule1)) -> rule5))]
The dog likes the lion.
("dog" "likes" "lion" "+")
triple1
The dog visits the lion.
("dog" "visits" "lion" "+")
triple2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple4
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple5
((triple7) -> (rule4 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
triple6
The lion visits the dog.
("lion" "visits" "dog" "+")
triple7
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple8
The mouse is green.
("mouse" "is" "green" "+")
triple9
The mouse is rough.
("mouse" "is" "rough" "+")
triple10
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple11
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple12
The dog needs the lion.
("dog" "needs" "lion" "+")
((triple3 triple12) -> (rule3 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
((triple8 triple12) -> (rule3 % int1))
The dog needs the lion.
("dog" "needs" "lion" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple12) -> (rule4 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((triple12 ((triple3 triple12) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
((triple12 ((triple8 triple12) -> (rule3 % int2))) -> (rule1 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The dog needs the lion.
("dog" "needs" "lion" "+")
int2
The mouse visits the lion.
("mouse" "visits" "lion" "+")
((((triple12 ((triple3 triple12) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The dog needs the lion.
("dog" "needs" "lion" "+")
int3
((((triple12 ((triple8 triple12) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The dog needs the lion.
("dog" "needs" "lion" "+")
int3