The cow is not nice. The cow visits the mouse. The cow visits the tiger. The mouse is big. The mouse is cold. The mouse is kind. The mouse needs the cow. The mouse sees the cow. The mouse sees the tiger. The mouse visits the cow. The mouse visits the tiger. The tiger needs the cow. The tiger needs the mouse. The tiger does not visit the cow. The tiger visits the mouse. If something visits the mouse and it is nice then it needs the tiger. If something visits the mouse then the mouse sees the cow. If something visits the cow then the cow needs the mouse. If something needs the mouse and the mouse does not need the cow then the mouse is not cold. If something is young and it sees the cow then the cow sees the tiger. If something sees the tiger then it is young. If the cow is nice then the cow is kind. If something sees the tiger and the tiger visits the cow then the tiger needs the mouse.
The cow is not nice.
("cow" "is" "nice" "-")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger needs the cow.
("tiger" "needs" "cow" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger does not visit the cow.
("tiger" "visits" "cow" "-")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If something visits the mouse and it is nice then it needs the tiger.
((("something" "visits" "mouse" "+") ("something" "is" "nice" "+")) -> ("something" "needs" "tiger" "+"))
If something visits the mouse then the mouse sees the cow.
((("something" "visits" "mouse" "+")) -> ("mouse" "sees" "cow" "+"))
If something visits the cow then the cow needs the mouse.
((("something" "visits" "cow" "+")) -> ("cow" "needs" "mouse" "+"))
If something needs the mouse and the mouse does not need the cow then the mouse is not cold.
((("something" "needs" "mouse" "+") ("mouse" "needs" "cow" "~")) -> ("mouse" "is" "cold" "-"))
If something is young and it sees the cow then the cow sees the tiger.
((("something" "is" "young" "+") ("something" "sees" "cow" "+")) -> ("cow" "sees" "tiger" "+"))
If something sees the tiger then it is young.
((("something" "sees" "tiger" "+")) -> ("something" "is" "young" "+"))
If the cow is nice then the cow is kind.
((("cow" "is" "nice" "+")) -> ("cow" "is" "kind" "+"))
If something sees the tiger and the tiger visits the cow then the tiger needs the mouse.
((("something" "sees" "tiger" "+") ("tiger" "visits" "cow" "+")) -> ("tiger" "needs" "mouse" "+"))
The mouse is kind.
True
1
proof
[(triple6)]
("mouse" "is" "kind" "+")
triple6
The tiger does not need the cow.
False
1
inv-proof
[(triple12)]
("tiger" "needs" "cow" "-")
triple12
The mouse is young.
True
2
proof
[(((triple9) -> rule6))]
("mouse" "is" "young" "+")
((triple9) -> (rule6 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse is not young.
False
2
inv-proof
[(((triple9) -> rule6))]
("mouse" "is" "young" "-")
((triple9) -> (rule6 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The cow sees the tiger.
True
4
proof
[(((((triple9) -> rule6) triple8) -> rule5) OR ((((triple9) -> rule6) ((triple15) -> rule2)) -> rule5) OR ((((triple9) -> rule6) ((triple2) -> rule2)) -> rule5))]
("cow" "sees" "tiger" "+")
((((triple9) -> (rule6 % int2)) triple8) -> (rule5 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
((((triple9) -> (rule6 % int3)) ((triple15) -> (rule2 % int2))) -> (rule5 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
((((triple9) -> (rule6 % int3)) ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The cow does not see the tiger.
False
4
inv-proof
[(((((triple9) -> rule6) triple8) -> rule5) OR ((((triple9) -> rule6) ((triple15) -> rule2)) -> rule5) OR ((((triple9) -> rule6) ((triple2) -> rule2)) -> rule5))]
("cow" "sees" "tiger" "-")
((((triple9) -> (rule6 % int2)) triple8) -> (rule5 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
((((triple9) -> (rule6 % int3)) ((triple15) -> (rule2 % int2))) -> (rule5 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
((((triple9) -> (rule6 % int3)) ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The cow is young.
True
5
proof
[(((((((triple9) -> rule6) triple8) -> rule5)) -> rule6) OR ((((((triple9) -> rule6) ((triple15) -> rule2)) -> rule5)) -> rule6) OR ((((((triple9) -> rule6) ((triple2) -> rule2)) -> rule5)) -> rule6))]
("cow" "is" "young" "+")
((((((triple9) -> (rule6 % int3)) triple8) -> (rule5 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
((((((triple9) -> (rule6 % int4)) ((triple15) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
int4
((((((triple9) -> (rule6 % int4)) ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
int4
The cow is not young.
False
5
inv-proof
[(((((((triple9) -> rule6) triple8) -> rule5)) -> rule6) OR ((((((triple9) -> rule6) ((triple15) -> rule2)) -> rule5)) -> rule6) OR ((((((triple9) -> rule6) ((triple2) -> rule2)) -> rule5)) -> rule6))]
("cow" "is" "young" "-")
((((((triple9) -> (rule6 % int3)) triple8) -> (rule5 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
((((((triple9) -> (rule6 % int4)) ((triple15) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
int4
((((((triple9) -> (rule6 % int4)) ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
int4
The mouse does not need the tiger.
Unknown
inv-rconc
[@1: The mouse needs the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "tiger" "-")
The tiger needs the tiger.
Unknown
rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "needs" "tiger" "+")
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "young" "-")
The cow is kind.
Unknown
rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "is" "kind" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
The cow does not see the mouse.
Unknown
inv-random
[@0: The cow sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "mouse" "-")
The tiger sees the mouse.
Unknown
random
[@0: The tiger sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "mouse" "+")
@0: The cow is not nice.[(triple1)] The cow visits the mouse.[(triple2)] The cow visits the tiger.[(triple3)] The mouse is big.[(triple4)] The mouse is cold.[(triple5)] The mouse is kind.[(triple6)] The mouse needs the cow.[(triple7)] The mouse sees the cow.[(triple8 OR ((triple15) -> rule2) OR ((triple2) -> rule2))] The mouse sees the tiger.[(triple9)] The mouse visits the cow.[(triple10)] The mouse visits the tiger.[(triple11)] The tiger does not visit the cow.[(triple14)] The tiger needs the cow.[(triple12)] The tiger needs the mouse.[(triple13)] The tiger visits the mouse.[(triple15)] @1: The cow needs the mouse.[(((triple10) -> rule3))] The mouse is young.[(((triple9) -> rule6))] @2: The cow sees the tiger.[(((((triple9) -> rule6) triple8) -> rule5) OR ((((triple9) -> rule6) ((triple15) -> rule2)) -> rule5) OR ((((triple9) -> rule6) ((triple2) -> rule2)) -> rule5))] @3: The cow is young.[(((((((triple9) -> rule6) triple8) -> rule5)) -> rule6) OR ((((((triple9) -> rule6) ((triple15) -> rule2)) -> rule5)) -> rule6) OR ((((((triple9) -> rule6) ((triple2) -> rule2)) -> rule5)) -> rule6))]
The cow is not nice.
("cow" "is" "nice" "-")
triple1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple2
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple3
The mouse is big.
("mouse" "is" "big" "+")
triple4
The mouse is cold.
("mouse" "is" "cold" "+")
triple5
The mouse is kind.
("mouse" "is" "kind" "+")
triple6
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple7
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple8
((triple15) -> (rule2 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
((triple2) -> (rule2 % int1))
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple9
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple10
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple11
The tiger does not visit the cow.
("tiger" "visits" "cow" "-")
triple14
The tiger needs the cow.
("tiger" "needs" "cow" "+")
triple12
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple13
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple15
The cow needs the mouse.
("cow" "needs" "mouse" "+")
((triple10) -> (rule3 % int1))
The cow needs the mouse.
("cow" "needs" "mouse" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
((triple9) -> (rule6 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
((((triple9) -> (rule6 % int2)) triple8) -> (rule5 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
((((triple9) -> (rule6 % int3)) ((triple15) -> (rule2 % int2))) -> (rule5 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
((((triple9) -> (rule6 % int3)) ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
The cow is young.
("cow" "is" "young" "+")
((((((triple9) -> (rule6 % int3)) triple8) -> (rule5 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The mouse is young.
("mouse" "is" "young" "+")
int3
((((((triple9) -> (rule6 % int4)) ((triple15) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
int4
((((((triple9) -> (rule6 % int4)) ((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int2
The mouse sees the cow.
("mouse" "sees" "cow" "+")
int3
The mouse is young.
("mouse" "is" "young" "+")
int4