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