The cat eats the mouse. The cat is not green. The cow eats the mouse. The cow eats the tiger. The mouse eats the cat. The mouse is big. The mouse does not need the cat. The mouse needs the tiger. The mouse visits the tiger. The tiger visits the cow. If something eats the mouse then the mouse is not green. If something needs the tiger and the tiger does not visit the mouse then the mouse does not visit the cow. If the mouse is big and the mouse is rough then the mouse needs the cow. If something eats the cow then it is blue. If something is blue and big then it is rough. If something visits the cow and it eats the mouse then the mouse does not need the cat. If the mouse is big then the mouse eats the cow. If the mouse needs the cow then the mouse does not eat the tiger. If something visits the cow and it does not eat the cow then it does not need the cow.
The cat eats the mouse.
("cat" "eats" "mouse" "+")
The cat is not green.
("cat" "is" "green" "-")
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something eats the mouse then the mouse is not green.
((("something" "eats" "mouse" "+")) -> ("mouse" "is" "green" "-"))
If something needs the tiger and the tiger does not visit the mouse then the mouse does not visit the cow.
((("something" "needs" "tiger" "+") ("tiger" "visits" "mouse" "~")) -> ("mouse" "visits" "cow" "-"))
If the mouse is big and the mouse is rough then the mouse needs the cow.
((("mouse" "is" "big" "+") ("mouse" "is" "rough" "+")) -> ("mouse" "needs" "cow" "+"))
If something eats the cow then it is blue.
((("something" "eats" "cow" "+")) -> ("something" "is" "blue" "+"))
If something is blue and big then it is rough.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something visits the cow and it eats the mouse then the mouse does not need the cat.
((("something" "visits" "cow" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "needs" "cat" "-"))
If the mouse is big then the mouse eats the cow.
((("mouse" "is" "big" "+")) -> ("mouse" "eats" "cow" "+"))
If the mouse needs the cow then the mouse does not eat the tiger.
((("mouse" "needs" "cow" "+")) -> ("mouse" "eats" "tiger" "-"))
If something visits the cow and it does not eat the cow then it does not need the cow.
((("something" "visits" "cow" "+") ("something" "eats" "cow" "~")) -> ("something" "needs" "cow" "-"))
The mouse visits the tiger.
True
1
proof
[(triple9)]
("mouse" "visits" "tiger" "+")
triple9
The mouse needs the cat.
False
1
inv-proof
[(triple7)]
("mouse" "needs" "cat" "+")
triple7
The mouse is not green.
True
2
proof
[(((triple1) -> rule1) OR ((triple3) -> rule1))]
("mouse" "is" "green" "-")
((triple1) -> (rule1 % int1))
The mouse is not green.
("mouse" "is" "green" "-")
int1
((triple3) -> (rule1 % int1))
The mouse is not green.
("mouse" "is" "green" "-")
int1
The mouse is green.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple3) -> rule1))]
("mouse" "is" "green" "+")
((triple1) -> (rule1 % int1))
The mouse is not green.
("mouse" "is" "green" "-")
int1
((triple3) -> (rule1 % int1))
The mouse is not green.
("mouse" "is" "green" "-")
int1
The mouse is blue.
True
3
proof
[(((((triple6) -> rule7)) -> rule4))]
("mouse" "is" "blue" "+")
((((triple6) -> (rule7 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
The mouse is not blue.
False
3
inv-proof
[(((((triple6) -> rule7)) -> rule4))]
("mouse" "is" "blue" "-")
((((triple6) -> (rule7 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
The mouse is rough.
True
5
proof
[(((((((triple6) -> rule7)) -> rule4) triple6) -> rule5))]
("mouse" "is" "rough" "+")
((((((triple6) -> (rule7 % int3))) -> (rule4 % int2)) triple6) -> (rule5 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int3
The mouse is not rough.
False
5
inv-proof
[(((((((triple6) -> rule7)) -> rule4) triple6) -> rule5))]
("mouse" "is" "rough" "-")
((((((triple6) -> (rule7 % int3))) -> (rule4 % int2)) triple6) -> (rule5 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int3
The mouse needs the cow.
True
7
proof
[(((triple6 ((((((triple6) -> rule7)) -> rule4) triple6) -> rule5)) -> rule3))]
("mouse" "needs" "cow" "+")
((triple6 ((((((triple6) -> (rule7 % int4))) -> (rule4 % int3)) triple6) -> (rule5 % int2))) -> (rule3 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int4
The mouse does not need the cow.
False
7
inv-proof
[(((triple6 ((((((triple6) -> rule7)) -> rule4) triple6) -> rule5)) -> rule3))]
("mouse" "needs" "cow" "-")
((triple6 ((((((triple6) -> (rule7 % int4))) -> (rule4 % int3)) triple6) -> (rule5 % int2))) -> (rule3 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int4
The mouse does not eat the tiger.
True
8
proof
[(((((triple6 ((((((triple6) -> rule7)) -> rule4) triple6) -> rule5)) -> rule3)) -> rule8))]
("mouse" "eats" "tiger" "-")
((((triple6 ((((((triple6) -> (rule7 % int5))) -> (rule4 % int4)) triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The mouse does not eat the tiger.
("mouse" "eats" "tiger" "-")
int1
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse is blue.
("mouse" "is" "blue" "+")
int4
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int5
The mouse eats the tiger.
False
8
inv-proof
[(((((triple6 ((((((triple6) -> rule7)) -> rule4) triple6) -> rule5)) -> rule3)) -> rule8))]
("mouse" "eats" "tiger" "+")
((((triple6 ((((((triple6) -> (rule7 % int5))) -> (rule4 % int4)) triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The mouse does not eat the tiger.
("mouse" "eats" "tiger" "-")
int1
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse is blue.
("mouse" "is" "blue" "+")
int4
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int5
The cat is not rough.
Unknown
inv-rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "rough" "-")
The tiger is blue.
Unknown
rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "blue" "+")
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "blue" "-")
The tiger is rough.
Unknown
rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "rough" "+")
The cow is not blue.
Unknown
inv-rconc
[@1: The cow is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "blue" "-")
The cow is rough.
Unknown
rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "rough" "+")
The cat does not visit the cow.
Unknown
inv-random
[@0: The cat visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cow" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat eats the tiger.
Unknown
random
[@0: The cat eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "tiger" "+")
The cat does not eat the cow.
Unknown
inv-random
[@0: The cat eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cow" "-")
The tiger needs the cow.
Unknown
random
[@0: The tiger needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "cow" "+")
@0: The cat eats the mouse.[(triple1)] The cat is not green.[(triple2)] The cow eats the mouse.[(triple3)] The cow eats the tiger.[(triple4)] The mouse does not need the cat.[(triple7)] The mouse eats the cat.[(triple5)] The mouse is big.[(triple6)] The mouse needs the tiger.[(triple8)] The mouse visits the tiger.[(triple9)] The tiger visits the cow.[(triple10)] @1: The mouse eats the cow.[(((triple6) -> rule7))] The mouse is not green.[(((triple1) -> rule1) OR ((triple3) -> rule1))] @2: The mouse is blue.[(((((triple6) -> rule7)) -> rule4))] @3: The mouse is rough.[(((((((triple6) -> rule7)) -> rule4) triple6) -> rule5))] @4: The mouse needs the cow.[(((triple6 ((((((triple6) -> rule7)) -> rule4) triple6) -> rule5)) -> rule3))] @5: The mouse does not eat the tiger.[(((((triple6 ((((((triple6) -> rule7)) -> rule4) triple6) -> rule5)) -> rule3)) -> rule8))]
The cat eats the mouse.
("cat" "eats" "mouse" "+")
triple1
The cat is not green.
("cat" "is" "green" "-")
triple2
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple3
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple4
The mouse does not need the cat.
("mouse" "needs" "cat" "-")
triple7
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple5
The mouse is big.
("mouse" "is" "big" "+")
triple6
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple8
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple9
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple10
The mouse eats the cow.
("mouse" "eats" "cow" "+")
((triple6) -> (rule7 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The mouse is not green.
("mouse" "is" "green" "-")
((triple1) -> (rule1 % int1))
The mouse is not green.
("mouse" "is" "green" "-")
int1
((triple3) -> (rule1 % int1))
The mouse is not green.
("mouse" "is" "green" "-")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
((((triple6) -> (rule7 % int2))) -> (rule4 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
((((((triple6) -> (rule7 % int3))) -> (rule4 % int2)) triple6) -> (rule5 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int3
The mouse needs the cow.
("mouse" "needs" "cow" "+")
((triple6 ((((((triple6) -> (rule7 % int4))) -> (rule4 % int3)) triple6) -> (rule5 % int2))) -> (rule3 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
int2
The mouse is blue.
("mouse" "is" "blue" "+")
int3
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int4
The mouse does not eat the tiger.
("mouse" "eats" "tiger" "-")
((((triple6 ((((((triple6) -> (rule7 % int5))) -> (rule4 % int4)) triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The mouse does not eat the tiger.
("mouse" "eats" "tiger" "-")
int1
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse is blue.
("mouse" "is" "blue" "+")
int4
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int5