The bear is rough. The bear is round. The bear visits the dog. The dog eats the mouse. The dog visits the bear. The lion needs the mouse. The lion visits the dog. The mouse eats the dog. The mouse eats the lion. The mouse is cold. The mouse visits the lion. If something eats the dog and the dog needs the bear then the bear needs the dog. If something visits the dog then it is young. If the bear eats the mouse and the mouse needs the bear then the bear visits the dog. If something is rough and it visits the dog then it needs the dog. If something eats the bear then it is rough. If something needs the lion then the lion eats the bear. If something eats the mouse then the mouse needs the lion. If the lion is young and the lion needs the dog then the lion visits the bear. If something eats the lion and it eats the mouse then the mouse needs the bear.
The bear is rough.
("bear" "is" "rough" "+")
The bear is round.
("bear" "is" "round" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If something eats the dog and the dog needs the bear then the bear needs the dog.
((("something" "eats" "dog" "+") ("dog" "needs" "bear" "+")) -> ("bear" "needs" "dog" "+"))
If something visits the dog then it is young.
((("something" "visits" "dog" "+")) -> ("something" "is" "young" "+"))
If the bear eats the mouse and the mouse needs the bear then the bear visits the dog.
((("bear" "eats" "mouse" "+") ("mouse" "needs" "bear" "+")) -> ("bear" "visits" "dog" "+"))
If something is rough and it visits the dog then it needs the dog.
((("something" "is" "rough" "+") ("something" "visits" "dog" "+")) -> ("something" "needs" "dog" "+"))
If something eats the bear then it is rough.
((("something" "eats" "bear" "+")) -> ("something" "is" "rough" "+"))
If something needs the lion then the lion eats the bear.
((("something" "needs" "lion" "+")) -> ("lion" "eats" "bear" "+"))
If something eats the mouse then the mouse needs the lion.
((("something" "eats" "mouse" "+")) -> ("mouse" "needs" "lion" "+"))
If the lion is young and the lion needs the dog then the lion visits the bear.
((("lion" "is" "young" "+") ("lion" "needs" "dog" "+")) -> ("lion" "visits" "bear" "+"))
If something eats the lion and it eats the mouse then the mouse needs the bear.
((("something" "eats" "lion" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "needs" "bear" "+"))
The bear is rough.
True
1
proof
[(triple1)]
("bear" "is" "rough" "+")
triple1
The bear is not round.
False
1
inv-proof
[(triple2)]
("bear" "is" "round" "-")
triple2
The lion is young.
True
2
proof
[(((triple7) -> rule2))]
("lion" "is" "young" "+")
((triple7) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The bear is not young.
False
2
inv-proof
[(((triple3) -> rule2))]
("bear" "is" "young" "-")
((triple3) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The lion eats the bear.
True
3
proof
[(((((triple4) -> rule7)) -> rule6))]
("lion" "eats" "bear" "+")
((((triple4) -> (rule7 % int2))) -> (rule6 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The lion does not eat the bear.
False
3
inv-proof
[(((((triple4) -> rule7)) -> rule6))]
("lion" "eats" "bear" "-")
((((triple4) -> (rule7 % int2))) -> (rule6 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The lion is rough.
True
4
proof
[(((((((triple4) -> rule7)) -> rule6)) -> rule5))]
("lion" "is" "rough" "+")
((((((triple4) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int3
The lion is not rough.
False
4
inv-proof
[(((((((triple4) -> rule7)) -> rule6)) -> rule5))]
("lion" "is" "rough" "-")
((((((triple4) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int3
The lion needs the dog.
True
6
proof
[(((((((((triple4) -> rule7)) -> rule6)) -> rule5) triple7) -> rule4))]
("lion" "needs" "dog" "+")
((((((((triple4) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) triple7) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int4
The lion does not need the dog.
False
6
inv-proof
[(((((((((triple4) -> rule7)) -> rule6)) -> rule5) triple7) -> rule4))]
("lion" "needs" "dog" "-")
((((((((triple4) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) triple7) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int4
The lion visits the bear.
True
9
proof
[(((((triple7) -> rule2) ((((((((triple4) -> rule7)) -> rule6)) -> rule5) triple7) -> rule4)) -> rule8))]
("lion" "visits" "bear" "+")
((((triple7) -> (rule2 % int6)) ((((((((triple4) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule5 % int3)) triple7) -> (rule4 % int2))) -> (rule8 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The lion eats the bear.
("lion" "eats" "bear" "+")
int4
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int5
The lion is young.
("lion" "is" "young" "+")
int6
The lion does not visit the bear.
False
9
inv-proof
[(((((triple7) -> rule2) ((((((((triple4) -> rule7)) -> rule6)) -> rule5) triple7) -> rule4)) -> rule8))]
("lion" "visits" "bear" "-")
((((triple7) -> (rule2 % int6)) ((((((((triple4) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule5 % int3)) triple7) -> (rule4 % int2))) -> (rule8 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The lion eats the bear.
("lion" "eats" "bear" "+")
int4
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int5
The lion is young.
("lion" "is" "young" "+")
int6
The mouse does not need the bear.
Unknown
inv-rconc
[@1: The mouse needs the bear.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("mouse" "needs" "bear" "-")
The mouse needs the dog.
Unknown
rconc
[@1: The mouse needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "needs" "dog" "+")
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "young" "-")
The dog needs the dog.
Unknown
rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "needs" "dog" "+")
The mouse is not rough.
Unknown
inv-rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "rough" "-")
The mouse is young.
Unknown
rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "young" "+")
The lion does not need the bear.
Unknown
inv-random
[@0: The lion needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "bear" "-")
The dog visits the mouse.
Unknown
random
[@0: The dog visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "mouse" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The bear eats the dog.
Unknown
random
[@0: The bear eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "dog" "+")
The dog does not need the bear.
Unknown
inv-random
[@0: The dog needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "bear" "-")
The bear visits the lion.
Unknown
random
[@0: The bear visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "lion" "+")
@0: The bear is rough.[(triple1)] The bear is round.[(triple2)] The bear visits the dog.[(triple3)] The dog eats the mouse.[(triple4)] The dog visits the bear.[(triple5)] The lion needs the mouse.[(triple6)] The lion visits the dog.[(triple7)] The mouse eats the dog.[(triple8)] The mouse eats the lion.[(triple9)] The mouse is cold.[(triple10)] The mouse visits the lion.[(triple11)] @1: The bear is young.[(((triple3) -> rule2))] The bear needs the dog.[(((triple1 triple3) -> rule4))] The lion is young.[(((triple7) -> rule2))] The mouse needs the lion.[(((triple4) -> rule7))] @2: The lion eats the bear.[(((((triple4) -> rule7)) -> rule6))] @3: The lion is rough.[(((((((triple4) -> rule7)) -> rule6)) -> rule5))] @4: The lion needs the dog.[(((((((((triple4) -> rule7)) -> rule6)) -> rule5) triple7) -> rule4))] @5: The lion visits the bear.[(((((triple7) -> rule2) ((((((((triple4) -> rule7)) -> rule6)) -> rule5) triple7) -> rule4)) -> rule8))]
The bear is rough.
("bear" "is" "rough" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
triple2
The bear visits the dog.
("bear" "visits" "dog" "+")
triple3
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple4
The dog visits the bear.
("dog" "visits" "bear" "+")
triple5
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple6
The lion visits the dog.
("lion" "visits" "dog" "+")
triple7
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple8
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple11
The bear is young.
("bear" "is" "young" "+")
((triple3) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
((triple1 triple3) -> (rule4 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The lion is young.
("lion" "is" "young" "+")
((triple7) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
((triple4) -> (rule7 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
((((triple4) -> (rule7 % int2))) -> (rule6 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
((((((triple4) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
int2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int3
The lion needs the dog.
("lion" "needs" "dog" "+")
((((((((triple4) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) triple7) -> (rule4 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion eats the bear.
("lion" "eats" "bear" "+")
int3
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int4
The lion visits the bear.
("lion" "visits" "bear" "+")
((((triple7) -> (rule2 % int6)) ((((((((triple4) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule5 % int3)) triple7) -> (rule4 % int2))) -> (rule8 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The lion eats the bear.
("lion" "eats" "bear" "+")
int4
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int5
The lion is young.
("lion" "is" "young" "+")
int6