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