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