The dog is cold. The dog needs the lion. The dog needs the mouse. The dog sees the mouse. The dog visits the lion. The dog visits the mouse. The lion is green. The lion is nice. The lion needs the dog. The lion sees the dog. The lion does not see the mouse. The mouse is big. The mouse is cold. The mouse sees the lion. The mouse does not visit the dog. If something visits the dog then it is green. If the lion needs the mouse then the lion is not green. If the lion is green then the lion does not visit the mouse. If something visits the dog and it is not cold then it visits the lion. If the mouse is cold and the mouse visits the lion then the lion is young. If something needs the lion then it does not visit the dog. If something sees the lion and it does not need the mouse then the mouse is young. If the dog needs the mouse and the lion does not visit the dog then the dog sees the lion.
The dog is cold.
("dog" "is" "cold" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion sees the dog.
("lion" "sees" "dog" "+")
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The mouse does not visit the dog.
("mouse" "visits" "dog" "-")
If something visits the dog then it is green.
((("something" "visits" "dog" "+")) -> ("something" "is" "green" "+"))
If the lion needs the mouse then the lion is not green.
((("lion" "needs" "mouse" "+")) -> ("lion" "is" "green" "-"))
If the lion is green then the lion does not visit the mouse.
((("lion" "is" "green" "+")) -> ("lion" "visits" "mouse" "-"))
If something visits the dog and it is not cold then it visits the lion.
((("something" "visits" "dog" "+") ("something" "is" "cold" "~")) -> ("something" "visits" "lion" "+"))
If the mouse is cold and the mouse visits the lion then the lion is young.
((("mouse" "is" "cold" "+") ("mouse" "visits" "lion" "+")) -> ("lion" "is" "young" "+"))
If something needs the lion then it does not visit the dog.
((("something" "needs" "lion" "+")) -> ("something" "visits" "dog" "-"))
If something sees the lion and it does not need the mouse then the mouse is young.
((("something" "sees" "lion" "+") ("something" "needs" "mouse" "~")) -> ("mouse" "is" "young" "+"))
If the dog needs the mouse and the lion does not visit the dog then the dog sees the lion.
((("dog" "needs" "mouse" "+") ("lion" "visits" "dog" "~")) -> ("dog" "sees" "lion" "+"))
The dog visits the mouse.
True
1
proof
[(triple6)]
("dog" "visits" "mouse" "+")
triple6
The dog does not see the mouse.
False
1
inv-proof
[(triple4)]
("dog" "sees" "mouse" "-")
triple4
The lion does not visit the mouse.
True
2
proof
[(((triple7) -> rule3))]
("lion" "visits" "mouse" "-")
((triple7) -> (rule3 % int1))
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
int1
The dog visits the dog.
False
2
inv-proof
[(((triple2) -> rule6))]
("dog" "visits" "dog" "+")
((triple2) -> (rule6 % int1))
The dog does not visit the dog.
("dog" "visits" "dog" "-")
int1
The lion is not young.
Unknown
inv-rconc
[@2: The lion is young.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("lion" "is" "young" "-")
The mouse is green.
Unknown
rconc
[@1: The mouse is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "green" "+")
The dog is not young.
Unknown
inv-random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "-")
The mouse needs the lion.
Unknown
random
[@0: The mouse needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "lion" "+")
@0: The dog is cold.[(triple1)] The dog needs the lion.[(triple2)] The dog needs the mouse.[(triple3)] The dog sees the mouse.[(triple4)] The dog visits the lion.[(triple5)] The dog visits the mouse.[(triple6)] The lion does not see the mouse.[(triple11)] The lion is green.[(triple7)] The lion is nice.[(triple8)] The lion needs the dog.[(triple9)] The lion sees the dog.[(triple10)] The mouse does not visit the dog.[(triple15)] The mouse is big.[(triple12)] The mouse is cold.[(triple13)] The mouse sees the lion.[(triple14)] @1: The dog does not visit the dog.[(((triple2) -> rule6))] The lion does not visit the mouse.[(((triple7) -> rule3))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
The dog needs the lion.
("dog" "needs" "lion" "+")
triple2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple3
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple4
The dog visits the lion.
("dog" "visits" "lion" "+")
triple5
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple6
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
triple11
The lion is green.
("lion" "is" "green" "+")
triple7
The lion is nice.
("lion" "is" "nice" "+")
triple8
The lion needs the dog.
("lion" "needs" "dog" "+")
triple9
The lion sees the dog.
("lion" "sees" "dog" "+")
triple10
The mouse does not visit the dog.
("mouse" "visits" "dog" "-")
triple15
The mouse is big.
("mouse" "is" "big" "+")
triple12
The mouse is cold.
("mouse" "is" "cold" "+")
triple13
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple14
The dog does not visit the dog.
("dog" "visits" "dog" "-")
((triple2) -> (rule6 % int1))
The dog does not visit the dog.
("dog" "visits" "dog" "-")
int1
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
((triple7) -> (rule3 % int1))
The lion does not visit the mouse.
("lion" "visits" "mouse" "-")
int1