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