The cow eats the lion. The cow is green. The cow is kind. The lion needs the rabbit. The mouse is young. The rabbit eats the lion. The rabbit is green. The rabbit likes the lion. The rabbit likes the mouse. The rabbit needs the lion. The rabbit needs the mouse. If someone needs the cow and the cow eats the mouse then the mouse is round. If the mouse likes the cow then the cow is young. If someone needs the rabbit then they need the mouse. If someone likes the mouse then they eat the rabbit. If someone needs the cow and they eat the rabbit then the cow likes the lion. If someone needs the cow and the cow is rough then they are round. If someone is rough and green then they need the cow. If the cow likes the lion then the cow is green. If someone likes the lion then they are rough.
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The mouse is young.
("mouse" "is" "young" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
If someone needs the cow and the cow eats the mouse then the mouse is round.
((("someone" "needs" "cow" "+") ("cow" "eats" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If the mouse likes the cow then the cow is young.
((("mouse" "likes" "cow" "+")) -> ("cow" "is" "young" "+"))
If someone needs the rabbit then they need the mouse.
((("someone" "needs" "rabbit" "+")) -> ("someone" "needs" "mouse" "+"))
If someone likes the mouse then they eat the rabbit.
((("someone" "likes" "mouse" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone needs the cow and they eat the rabbit then the cow likes the lion.
((("someone" "needs" "cow" "+") ("someone" "eats" "rabbit" "+")) -> ("cow" "likes" "lion" "+"))
If someone needs the cow and the cow is rough then they are round.
((("someone" "needs" "cow" "+") ("cow" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If someone is rough and green then they need the cow.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "needs" "cow" "+"))
If the cow likes the lion then the cow is green.
((("cow" "likes" "lion" "+")) -> ("cow" "is" "green" "+"))
If someone likes the lion then they are rough.
((("someone" "likes" "lion" "+")) -> ("someone" "is" "rough" "+"))
The cow is kind.
True
1
proof
[(triple3)]
("cow" "is" "kind" "+")
triple3
The cow is not kind.
False
1
inv-proof
[(triple3)]
("cow" "is" "kind" "-")
triple3
The rabbit is rough.
True
2
proof
[(((triple8) -> rule9))]
("rabbit" "is" "rough" "+")
((triple8) -> (rule9 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit does not eat the rabbit.
False
2
inv-proof
[(((triple9) -> rule4))]
("rabbit" "eats" "rabbit" "-")
((triple9) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the cow.
True
4
proof
[(((((triple8) -> rule9) triple7) -> rule7))]
("rabbit" "needs" "cow" "+")
((((triple8) -> (rule9 % int2)) triple7) -> (rule7 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit does not need the cow.
False
4
inv-proof
[(((((triple8) -> rule9) triple7) -> rule7))]
("rabbit" "needs" "cow" "-")
((((triple8) -> (rule9 % int2)) triple7) -> (rule7 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow likes the lion.
True
7
proof
[(((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5))]
("cow" "likes" "lion" "+")
((((((triple8) -> (rule9 % int4)) triple7) -> (rule7 % int3)) ((triple9) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int3
The rabbit is rough.
("rabbit" "is" "rough" "+")
int4
The cow does not like the lion.
False
7
inv-proof
[(((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5))]
("cow" "likes" "lion" "-")
((((((triple8) -> (rule9 % int4)) triple7) -> (rule7 % int3)) ((triple9) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int3
The rabbit is rough.
("rabbit" "is" "rough" "+")
int4
The cow is rough.
True
8
proof
[(((((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5)) -> rule9))]
("cow" "is" "rough" "+")
((((((((triple8) -> (rule9 % int5)) triple7) -> (rule7 % int4)) ((triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
The rabbit is rough.
("rabbit" "is" "rough" "+")
int5
The cow is not rough.
False
8
inv-proof
[(((((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5)) -> rule9))]
("cow" "is" "rough" "-")
((((((((triple8) -> (rule9 % int5)) triple7) -> (rule7 % int4)) ((triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
The rabbit is rough.
("rabbit" "is" "rough" "+")
int5
The rabbit is round.
True
13
proof
[(((((((triple8) -> rule9) triple7) -> rule7) ((((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5)) -> rule9)) -> rule6))]
("rabbit" "is" "round" "+")
((((((triple8) -> (rule9 % int6)) triple7) -> (rule7 % int5)) ((((((((triple8) -> (rule9 % int6)) triple7) -> (rule7 % int5)) ((triple9) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow likes the lion.
("cow" "likes" "lion" "+")
int3
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int4
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int5
The rabbit is rough.
("rabbit" "is" "rough" "+")
int6
The rabbit is not round.
False
13
inv-proof
[(((((((triple8) -> rule9) triple7) -> rule7) ((((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5)) -> rule9)) -> rule6))]
("rabbit" "is" "round" "-")
((((((triple8) -> (rule9 % int6)) triple7) -> (rule7 % int5)) ((((((((triple8) -> (rule9 % int6)) triple7) -> (rule7 % int5)) ((triple9) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow likes the lion.
("cow" "likes" "lion" "+")
int3
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int4
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int5
The rabbit is rough.
("rabbit" "is" "rough" "+")
int6
The mouse is not rough.
Unknown
inv-rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("mouse" "is" "rough" "-")
The cow eats the rabbit.
Unknown
rconc
[@1: The cow eats the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "eats" "rabbit" "+")
The mouse is not round.
Unknown
inv-rconc
[@2: The mouse is round.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("mouse" "is" "round" "-")
The lion is rough.
Unknown
rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("lion" "is" "rough" "+")
The mouse does not need the cow.
Unknown
inv-rconc
[@1: The mouse needs the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "needs" "cow" "-")
The lion is round.
Unknown
rconc
[@2: The lion is round.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("lion" "is" "round" "+")
The cow does not like the mouse.
Unknown
inv-random
[@0: The cow likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "mouse" "-")
The cow likes the rabbit.
Unknown
random
[@0: The cow likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "rabbit" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The lion likes the cow.
Unknown
random
[@0: The lion likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cow" "+")
@0: The cow eats the lion.[(triple1)] The cow is green.[(triple2 OR ((((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5)) -> rule8))] The cow is kind.[(triple3)] The lion needs the rabbit.[(triple4)] The mouse is young.[(triple5)] The rabbit eats the lion.[(triple6)] The rabbit is green.[(triple7)] The rabbit likes the lion.[(triple8)] The rabbit likes the mouse.[(triple9)] The rabbit needs the lion.[(triple10)] The rabbit needs the mouse.[(triple11)] @1: The lion needs the mouse.[(((triple4) -> rule3))] The rabbit eats the rabbit.[(((triple9) -> rule4))] The rabbit is rough.[(((triple8) -> rule9))] @2: The rabbit needs the cow.[(((((triple8) -> rule9) triple7) -> rule7))] @3: The cow likes the lion.[(((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5))] @4: The cow is rough.[(((((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5)) -> rule9))] @5: The cow needs the cow.[(((((((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5)) -> rule9) triple2) -> rule7) OR ((((((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5)) -> rule9) ((((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5)) -> rule8)) -> rule7))] The rabbit is round.[(((((((triple8) -> rule9) triple7) -> rule7) ((((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5)) -> rule9)) -> rule6))] @6: The cow is round.[(((((((((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5)) -> rule9) triple2) -> rule7) ((((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5)) -> rule9)) -> rule6) OR ((((((((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5)) -> rule9) ((((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5)) -> rule8)) -> rule7) ((((((((triple8) -> rule9) triple7) -> rule7) ((triple9) -> rule4)) -> rule5)) -> rule9)) -> rule6))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The cow is green.
("cow" "is" "green" "+")
triple2
((((((((triple8) -> (rule9 % int5)) triple7) -> (rule7 % int4)) ((triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
The rabbit is rough.
("rabbit" "is" "rough" "+")
int5
The cow is kind.
("cow" "is" "kind" "+")
triple3
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple4
The mouse is young.
("mouse" "is" "young" "+")
triple5
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple6
The rabbit is green.
("rabbit" "is" "green" "+")
triple7
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple8
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple9
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple10
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple11
The lion needs the mouse.
("lion" "needs" "mouse" "+")
((triple4) -> (rule3 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple9) -> (rule4 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple8) -> (rule9 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
((((triple8) -> (rule9 % int2)) triple7) -> (rule7 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cow likes the lion.
("cow" "likes" "lion" "+")
((((((triple8) -> (rule9 % int4)) triple7) -> (rule7 % int3)) ((triple9) -> (rule4 % int2))) -> (rule5 % int1))
The cow likes the lion.
("cow" "likes" "lion" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int3
The rabbit is rough.
("rabbit" "is" "rough" "+")
int4
The cow is rough.
("cow" "is" "rough" "+")
((((((((triple8) -> (rule9 % int5)) triple7) -> (rule7 % int4)) ((triple9) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule9 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow likes the lion.
("cow" "likes" "lion" "+")
int2
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
The rabbit is rough.
("rabbit" "is" "rough" "+")
int5
The cow needs the cow.
("cow" "needs" "cow" "+")
((((((((((triple8) -> (rule9 % int6)) triple7) -> (rule7 % int5)) ((triple9) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule9 % int2)) triple2) -> (rule7 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow likes the lion.
("cow" "likes" "lion" "+")
int3
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int4
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int5
The rabbit is rough.
("rabbit" "is" "rough" "+")
int6
((((((((((triple8) -> (rule9 % int7)) triple7) -> (rule7 % int6)) ((triple9) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule9 % int3)) ((((((((triple8) -> (rule9 % int7)) triple7) -> (rule7 % int6)) ((triple9) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule8 % int2))) -> (rule7 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow likes the lion.
("cow" "likes" "lion" "+")
int4
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int5
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int6
The rabbit is rough.
("rabbit" "is" "rough" "+")
int7
The rabbit is round.
("rabbit" "is" "round" "+")
((((((triple8) -> (rule9 % int6)) triple7) -> (rule7 % int5)) ((((((((triple8) -> (rule9 % int6)) triple7) -> (rule7 % int5)) ((triple9) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow likes the lion.
("cow" "likes" "lion" "+")
int3
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int4
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int5
The rabbit is rough.
("rabbit" "is" "rough" "+")
int6
The cow is round.
("cow" "is" "round" "+")
((((((((((((triple8) -> (rule9 % int7)) triple7) -> (rule7 % int6)) ((triple9) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule9 % int3)) triple2) -> (rule7 % int2)) ((((((((triple8) -> (rule9 % int7)) triple7) -> (rule7 % int6)) ((triple9) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule9 % int3))) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
int3
The cow likes the lion.
("cow" "likes" "lion" "+")
int4
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int5
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int6
The rabbit is rough.
("rabbit" "is" "rough" "+")
int7
((((((((((((triple8) -> (rule9 % int8)) triple7) -> (rule7 % int7)) ((triple9) -> (rule4 % int6))) -> (rule5 % int5))) -> (rule9 % int4)) ((((((((triple8) -> (rule9 % int8)) triple7) -> (rule7 % int7)) ((triple9) -> (rule4 % int6))) -> (rule5 % int5))) -> (rule8 % int3))) -> (rule7 % int2)) ((((((((triple8) -> (rule9 % int8)) triple7) -> (rule7 % int7)) ((triple9) -> (rule4 % int6))) -> (rule5 % int5))) -> (rule9 % int4))) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow is rough.
("cow" "is" "rough" "+")
int4
The cow likes the lion.
("cow" "likes" "lion" "+")
int5
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int6
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int7
The rabbit is rough.
("rabbit" "is" "rough" "+")
int8