The lion likes the mouse. The mouse is big. The mouse is kind. If someone likes the mouse then the mouse likes the lion. All green people are rough. If someone likes the mouse then they like the lion. If someone likes the lion and the lion eats the mouse then the lion is big. If someone likes the lion then the lion is big. If the lion is young then the lion likes the mouse. If someone likes the lion and the lion is big then the lion is green. If someone is rough and they eat the mouse then they like the mouse.
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
If someone likes the mouse then the mouse likes the lion.
((("someone" "likes" "mouse" "+")) -> ("mouse" "likes" "lion" "+"))
All green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone likes the mouse then they like the lion.
((("someone" "likes" "mouse" "+")) -> ("someone" "likes" "lion" "+"))
If someone likes the lion and the lion eats the mouse then the lion is big.
((("someone" "likes" "lion" "+") ("lion" "eats" "mouse" "+")) -> ("lion" "is" "big" "+"))
If someone likes the lion then the lion is big.
((("someone" "likes" "lion" "+")) -> ("lion" "is" "big" "+"))
If the lion is young then the lion likes the mouse.
((("lion" "is" "young" "+")) -> ("lion" "likes" "mouse" "+"))
If someone likes the lion and the lion is big then the lion is green.
((("someone" "likes" "lion" "+") ("lion" "is" "big" "+")) -> ("lion" "is" "green" "+"))
If someone is rough and they eat the mouse then they like the mouse.
((("someone" "is" "rough" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "likes" "mouse" "+"))
The mouse is kind.
True
1
proof
[(triple3)]
("mouse" "is" "kind" "+")
triple3
The mouse is not kind.
False
1
inv-proof
[(triple3)]
("mouse" "is" "kind" "-")
triple3
The lion likes the lion.
True
2
proof
[(((triple1) -> rule3))]
("lion" "likes" "lion" "+")
((triple1) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The mouse does not like the lion.
False
2
inv-proof
[(((triple1) -> rule1))]
("mouse" "likes" "lion" "-")
((triple1) -> (rule1 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The lion is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule5) OR ((((triple1) -> rule3)) -> rule5))]
("lion" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5) OR ((((triple1) -> rule3)) -> rule5))]
("lion" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The mouse is not rough.
Unknown
inv-rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "rough" "-")
The mouse likes the mouse.
Unknown
rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "likes" "mouse" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The lion likes the mouse.[(triple1)] The mouse is big.[(triple2)] The mouse is kind.[(triple3)] @1: The lion likes the lion.[(((triple1) -> rule3))] The mouse likes the lion.[(((triple1) -> rule1))] @2: The lion is big.[(((((triple1) -> rule1)) -> rule5) OR ((((triple1) -> rule3)) -> rule5))] @3: The lion is green.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule5)) -> rule7) OR ((((triple1) -> rule1) ((((triple1) -> rule3)) -> rule5)) -> rule7) OR ((((triple1) -> rule3) ((((triple1) -> rule1)) -> rule5)) -> rule7) OR ((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule7))] @4: The lion is rough.[(((((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule5)) -> rule7)) -> rule2) OR ((((((triple1) -> rule1) ((((triple1) -> rule3)) -> rule5)) -> rule7)) -> rule2) OR ((((((triple1) -> rule3) ((((triple1) -> rule1)) -> rule5)) -> rule7)) -> rule2) OR ((((((triple1) -> rule3) ((((triple1) -> rule3)) -> rule5)) -> rule7)) -> rule2))]
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
The lion likes the lion.
("lion" "likes" "lion" "+")
((triple1) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
((triple1) -> (rule1 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion is green.
("lion" "is" "green" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int3
((((triple1) -> (rule1 % int4)) ((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int4
((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int3
The lion likes the lion.
("lion" "likes" "lion" "+")
int4
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
((((((triple1) -> (rule1 % int4)) ((((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int4
((((((triple1) -> (rule1 % int5)) ((((triple1) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion likes the lion.
("lion" "likes" "lion" "+")
int4
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int5
((((((triple1) -> (rule3 % int5)) ((((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int4
The lion likes the lion.
("lion" "likes" "lion" "+")
int5
((((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule3 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion likes the lion.
("lion" "likes" "lion" "+")
int4