The cow sees the lion. The lion sees the tiger. The mouse is round. The tiger is big. If something eats the lion then it sees the tiger. If the cow does not eat the tiger then the tiger does not see the mouse. If something sees the tiger then the tiger sees the mouse. If the tiger needs the mouse then the tiger is not big. If something eats the lion then it is red. If something sees the mouse then it eats the lion. If something is round then it eats the lion. If something eats the lion and it is big then it sees the lion.
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The mouse is round.
("mouse" "is" "round" "+")
The tiger is big.
("tiger" "is" "big" "+")
If something eats the lion then it sees the tiger.
((("something" "eats" "lion" "+")) -> ("something" "sees" "tiger" "+"))
If the cow does not eat the tiger then the tiger does not see the mouse.
((("cow" "eats" "tiger" "~")) -> ("tiger" "sees" "mouse" "-"))
If something sees the tiger then the tiger sees the mouse.
((("something" "sees" "tiger" "+")) -> ("tiger" "sees" "mouse" "+"))
If the tiger needs the mouse then the tiger is not big.
((("tiger" "needs" "mouse" "+")) -> ("tiger" "is" "big" "-"))
If something eats the lion then it is red.
((("something" "eats" "lion" "+")) -> ("something" "is" "red" "+"))
If something sees the mouse then it eats the lion.
((("something" "sees" "mouse" "+")) -> ("something" "eats" "lion" "+"))
If something is round then it eats the lion.
((("something" "is" "round" "+")) -> ("something" "eats" "lion" "+"))
If something eats the lion and it is big then it sees the lion.
((("something" "eats" "lion" "+") ("something" "is" "big" "+")) -> ("something" "sees" "lion" "+"))
The cow sees the lion.
True
1
proof
[(triple1)]
("cow" "sees" "lion" "+")
triple1
The lion does not see the tiger.
False
1
inv-proof
[(triple2)]
("lion" "sees" "tiger" "-")
triple2
The tiger sees the mouse.
True
2
proof
[(((triple2) -> rule3) OR ((((((triple3) -> rule7)) -> rule1)) -> rule3))]
("tiger" "sees" "mouse" "+")
((triple2) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The tiger does not see the mouse.
False
2
inv-proof
[(((triple2) -> rule3) OR ((((((triple3) -> rule7)) -> rule1)) -> rule3))]
("tiger" "sees" "mouse" "-")
((triple2) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The mouse sees the tiger.
True
3
proof
[(((((triple3) -> rule7)) -> rule1))]
("mouse" "sees" "tiger" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The mouse is not red.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule5))]
("mouse" "is" "red" "-")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The tiger is red.
True
4
proof
[(((((((triple2) -> rule3)) -> rule6)) -> rule5) OR ((((((((((triple3) -> rule7)) -> rule1)) -> rule3)) -> rule6)) -> rule5))]
("tiger" "is" "red" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
((((((((((triple3) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int5
The tiger is not red.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule6)) -> rule5) OR ((((((((((triple3) -> rule7)) -> rule1)) -> rule3)) -> rule6)) -> rule5))]
("tiger" "is" "red" "-")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
((((((((((triple3) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int5
The lion does not see the lion.
Unknown
inv-rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "sees" "lion" "-")
The cow is red.
Unknown
rconc
[@2: The cow is red.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("cow" "is" "red" "+")
The lion does not eat the lion.
Unknown
inv-rconc
[@1: The lion eats the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "eats" "lion" "-")
The cow sees the tiger.
Unknown
rconc
[@2: The cow sees the tiger.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("cow" "sees" "tiger" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
The mouse does not see the cow.
Unknown
inv-random
[@0: The mouse sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "cow" "-")
The lion eats the mouse.
Unknown
random
[@0: The lion eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "mouse" "+")
@0: The cow sees the lion.[(triple1)] The lion sees the tiger.[(triple2)] The mouse is round.[(triple3)] The tiger is big.[(triple4)] @1: The mouse eats the lion.[(((triple3) -> rule7))] The tiger sees the mouse.[(((triple2) -> rule3) OR ((((((triple3) -> rule7)) -> rule1)) -> rule3))] @2: The mouse is red.[(((((triple3) -> rule7)) -> rule5))] The mouse sees the tiger.[(((((triple3) -> rule7)) -> rule1))] The tiger eats the lion.[(((((triple2) -> rule3)) -> rule6) OR ((((((((triple3) -> rule7)) -> rule1)) -> rule3)) -> rule6))] @3: The tiger is red.[(((((((triple2) -> rule3)) -> rule6)) -> rule5) OR ((((((((((triple3) -> rule7)) -> rule1)) -> rule3)) -> rule6)) -> rule5))] The tiger sees the lion.[(((((((triple2) -> rule3)) -> rule6) triple4) -> rule8) OR ((((((((((triple3) -> rule7)) -> rule1)) -> rule3)) -> rule6) triple4) -> rule8))] The tiger sees the tiger.[(((((((triple2) -> rule3)) -> rule6)) -> rule1) OR ((((((((((triple3) -> rule7)) -> rule1)) -> rule3)) -> rule6)) -> rule1))]
The cow sees the lion.
("cow" "sees" "lion" "+")
triple1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple2
The mouse is round.
("mouse" "is" "round" "+")
triple3
The tiger is big.
("tiger" "is" "big" "+")
triple4
The mouse eats the lion.
("mouse" "eats" "lion" "+")
((triple3) -> (rule7 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
((triple2) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
((((((triple3) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The tiger eats the lion.
("tiger" "eats" "lion" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
((((((((triple3) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int2
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int3
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int4
The tiger is red.
("tiger" "is" "red" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
((((((((((triple3) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int5
The tiger sees the lion.
("tiger" "sees" "lion" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2)) triple4) -> (rule8 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
((((((((((triple3) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) triple4) -> (rule8 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int5
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
((((((((((triple3) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int3
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
int4
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int5