The bear is not blue. The bear is green. The bear needs the mouse. The bear needs the tiger. The dog chases the mouse. The dog chases the tiger. The dog sees the tiger. The mouse needs the bear. The tiger chases the bear. The tiger needs the bear. The tiger does not see the bear. If something sees the mouse and it needs the dog then it is rough. If the tiger needs the dog then the dog is green. If something is round and rough then it chases the mouse. If something chases the dog and the dog sees the tiger then the dog is not round. If something sees the mouse and it chases the tiger then the mouse needs the dog. If something chases the mouse then it needs the mouse. If something is green then it sees the mouse. If something needs the dog then it does not see the mouse. If something needs the tiger then the tiger needs the dog.
The bear is not blue.
("bear" "is" "blue" "-")
The bear is green.
("bear" "is" "green" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger does not see the bear.
("tiger" "sees" "bear" "-")
If something sees the mouse and it needs the dog then it is rough.
((("something" "sees" "mouse" "+") ("something" "needs" "dog" "+")) -> ("something" "is" "rough" "+"))
If the tiger needs the dog then the dog is green.
((("tiger" "needs" "dog" "+")) -> ("dog" "is" "green" "+"))
If something is round and rough then it chases the mouse.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "chases" "mouse" "+"))
If something chases the dog and the dog sees the tiger then the dog is not round.
((("something" "chases" "dog" "+") ("dog" "sees" "tiger" "+")) -> ("dog" "is" "round" "-"))
If something sees the mouse and it chases the tiger then the mouse needs the dog.
((("something" "sees" "mouse" "+") ("something" "chases" "tiger" "+")) -> ("mouse" "needs" "dog" "+"))
If something chases the mouse then it needs the mouse.
((("something" "chases" "mouse" "+")) -> ("something" "needs" "mouse" "+"))
If something is green then it sees the mouse.
((("something" "is" "green" "+")) -> ("something" "sees" "mouse" "+"))
If something needs the dog then it does not see the mouse.
((("something" "needs" "dog" "+")) -> ("something" "sees" "mouse" "-"))
If something needs the tiger then the tiger needs the dog.
((("something" "needs" "tiger" "+")) -> ("tiger" "needs" "dog" "+"))
The dog sees the tiger.
True
1
proof
[(triple7)]
("dog" "sees" "tiger" "+")
triple7
The bear does not need the mouse.
False
1
inv-proof
[(triple3)]
("bear" "needs" "mouse" "-")
triple3
The tiger needs the dog.
True
2
proof
[(((triple4) -> rule9))]
("tiger" "needs" "dog" "+")
((triple4) -> (rule9 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The bear does not see the mouse.
False
2
inv-proof
[(((triple2) -> rule7))]
("bear" "sees" "mouse" "-")
((triple2) -> (rule7 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The dog is green.
True
3
proof
[(((((triple4) -> rule9)) -> rule2))]
("dog" "is" "green" "+")
((((triple4) -> (rule9 % int2))) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The dog is not green.
False
3
inv-proof
[(((((triple4) -> rule9)) -> rule2))]
("dog" "is" "green" "-")
((((triple4) -> (rule9 % int2))) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The dog sees the mouse.
True
4
proof
[(((((((triple4) -> rule9)) -> rule2)) -> rule7))]
("dog" "sees" "mouse" "+")
((((((triple4) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3
The dog does not see the mouse.
False
4
inv-proof
[(((((((triple4) -> rule9)) -> rule2)) -> rule7))]
("dog" "sees" "mouse" "-")
((((((triple4) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3
The mouse needs the dog.
True
6
proof
[(((((((((triple4) -> rule9)) -> rule2)) -> rule7) triple6) -> rule5))]
("mouse" "needs" "dog" "+")
((((((((triple4) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule7 % int2)) triple6) -> (rule5 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog is green.
("dog" "is" "green" "+")
int3
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int4
The mouse does not need the dog.
False
6
inv-proof
[(((((((((triple4) -> rule9)) -> rule2)) -> rule7) triple6) -> rule5))]
("mouse" "needs" "dog" "-")
((((((((triple4) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule7 % int2)) triple6) -> (rule5 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog is green.
("dog" "is" "green" "+")
int3
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int4
The mouse does not see the mouse.
True
7
proof
[(((((((((((triple4) -> rule9)) -> rule2)) -> rule7) triple6) -> rule5)) -> rule8))]
("mouse" "sees" "mouse" "-")
((((((((((triple4) -> (rule9 % int5))) -> (rule2 % int4))) -> (rule7 % int3)) triple6) -> (rule5 % int2))) -> (rule8 % int1))
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3
The dog is green.
("dog" "is" "green" "+")
int4
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int5
The mouse sees the mouse.
False
7
inv-proof
[(((((((((((triple4) -> rule9)) -> rule2)) -> rule7) triple6) -> rule5)) -> rule8))]
("mouse" "sees" "mouse" "+")
((((((((((triple4) -> (rule9 % int5))) -> (rule2 % int4))) -> (rule7 % int3)) triple6) -> (rule5 % int2))) -> (rule8 % int1))
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3
The dog is green.
("dog" "is" "green" "+")
int4
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int5
The mouse is not rough.
Unknown
inv-rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "rough" "-")
The mouse needs the mouse.
Unknown
rconc
[@2: The mouse needs the mouse.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse does not chase the mouse.
Unknown
inv-rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The tiger needs the mouse.
Unknown
rconc
[@2: The tiger needs the mouse.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("tiger" "needs" "mouse" "+")
The tiger does not chase the mouse.
Unknown
inv-rconc
[@1: The tiger chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "chases" "mouse" "-")
The dog is rough.
Unknown
rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "rough" "+")
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The mouse does not chase the tiger.
Unknown
inv-random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The mouse sees the dog.
Unknown
random
[@0: The mouse sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "dog" "+")
@0: The bear is green.[(triple2)] The bear is not blue.[(triple1)] The bear needs the mouse.[(triple3)] The bear needs the tiger.[(triple4)] The dog chases the mouse.[(triple5)] The dog chases the tiger.[(triple6)] The dog sees the tiger.[(triple7)] The mouse needs the bear.[(triple8)] The tiger chases the bear.[(triple9)] The tiger does not see the bear.[(triple11)] The tiger needs the bear.[(triple10)] @1: The bear sees the mouse.[(((triple2) -> rule7))] The dog needs the mouse.[(((triple5) -> rule6))] The tiger needs the dog.[(((triple4) -> rule9))] @2: The dog is green.[(((((triple4) -> rule9)) -> rule2))] The tiger does not see the mouse.[(((((triple4) -> rule9)) -> rule8))] @3: The dog sees the mouse.[(((((((triple4) -> rule9)) -> rule2)) -> rule7))] @4: The mouse needs the dog.[(((((((((triple4) -> rule9)) -> rule2)) -> rule7) triple6) -> rule5))] @5: The mouse does not see the mouse.[(((((((((((triple4) -> rule9)) -> rule2)) -> rule7) triple6) -> rule5)) -> rule8))]
The bear is green.
("bear" "is" "green" "+")
triple2
The bear is not blue.
("bear" "is" "blue" "-")
triple1
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple3
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple4
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple5
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple6
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple7
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple8
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple9
The tiger does not see the bear.
("tiger" "sees" "bear" "-")
triple11
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple10
The bear sees the mouse.
("bear" "sees" "mouse" "+")
((triple2) -> (rule7 % int1))
The bear sees the mouse.
("bear" "sees" "mouse" "+")
int1
The dog needs the mouse.
("dog" "needs" "mouse" "+")
((triple5) -> (rule6 % int1))
The dog needs the mouse.
("dog" "needs" "mouse" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
((triple4) -> (rule9 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The dog is green.
("dog" "is" "green" "+")
((((triple4) -> (rule9 % int2))) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger does not see the mouse.
("tiger" "sees" "mouse" "-")
((((triple4) -> (rule9 % int2))) -> (rule8 % int1))
The tiger does not see the mouse.
("tiger" "sees" "mouse" "-")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
((((((triple4) -> (rule9 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
((((((((triple4) -> (rule9 % int4))) -> (rule2 % int3))) -> (rule7 % int2)) triple6) -> (rule5 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int2
The dog is green.
("dog" "is" "green" "+")
int3
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int4
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
((((((((((triple4) -> (rule9 % int5))) -> (rule2 % int4))) -> (rule7 % int3)) triple6) -> (rule5 % int2))) -> (rule8 % int1))
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
int3
The dog is green.
("dog" "is" "green" "+")
int4
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int5