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