The lion is big. The lion is green. The lion is kind. The lion is nice. The lion is rough. Big, nice people are kind. All big people are kind. If someone is kind then they are rough. Nice, green people are rough. If the lion is nice and the lion is kind then the lion is big. If the lion is rough and the lion is big then the lion is nice. Green, nice people are big. All big, rough people are nice.
The lion is big.
("lion" "is" "big" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
Big, nice people are kind.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind then they are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
Nice, green people are rough.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If the lion is nice and the lion is kind then the lion is big.
((("lion" "is" "nice" "+") ("lion" "is" "kind" "+")) -> ("lion" "is" "big" "+"))
If the lion is rough and the lion is big then the lion is nice.
((("lion" "is" "rough" "+") ("lion" "is" "big" "+")) -> ("lion" "is" "nice" "+"))
Green, nice people are big.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
All big, rough people are nice.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
The lion is big.
True
1
proof
[(triple1 OR ((triple2 triple4) -> rule7) OR ((triple4 triple3) -> rule5))]
("lion" "is" "big" "+")
triple1
((triple2 triple4) -> (rule7 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple4 triple3) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is not big.
False
1
inv-proof
[(triple1 OR ((triple2 triple4) -> rule7) OR ((triple4 triple3) -> rule5))]
("lion" "is" "big" "-")
triple1
((triple2 triple4) -> (rule7 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple4 triple3) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The lion is big.[(triple1 OR ((triple2 triple4) -> rule7) OR ((triple4 triple3) -> rule5))] The lion is green.[(triple2)] The lion is kind.[(triple3 OR ((triple1) -> rule2) OR ((triple1 triple4) -> rule1) OR ((((triple2 triple4) -> rule7)) -> rule2) OR ((triple1 ((triple1 triple5) -> rule8)) -> rule1) OR ((triple1 ((triple5 triple1) -> rule6)) -> rule1) OR ((((triple2 triple4) -> rule7) triple4) -> rule1) OR ((((triple2 triple4) -> rule7) ((triple1 triple5) -> rule8)) -> rule1) OR ((((triple2 triple4) -> rule7) ((triple5 triple1) -> rule6)) -> rule1))] The lion is nice.[(triple4 OR ((triple1 triple5) -> rule8) OR ((triple5 triple1) -> rule6) OR ((triple1 ((triple3) -> rule3)) -> rule8) OR ((((triple3) -> rule3) triple1) -> rule6) OR ((triple1 ((((triple1) -> rule2)) -> rule3)) -> rule8) OR ((((((triple1) -> rule2)) -> rule3) triple1) -> rule6))] The lion is rough.[(triple5 OR ((triple3) -> rule3) OR ((triple4 triple2) -> rule4) OR ((((triple1) -> rule2)) -> rule3) OR ((((triple1 triple4) -> rule1)) -> rule3) OR ((((((triple2 triple4) -> rule7)) -> rule2)) -> rule3) OR ((((((triple2 triple4) -> rule7) triple4) -> rule1)) -> rule3))]
The lion is big.
("lion" "is" "big" "+")
triple1
((triple2 triple4) -> (rule7 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple4 triple3) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is green.
("lion" "is" "green" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
((triple1) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple1 triple4) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((((triple2 triple4) -> (rule7 % int2))) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
((triple1 ((triple1 triple5) -> (rule8 % int2))) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
((triple1 ((triple5 triple1) -> (rule6 % int2))) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
((((triple2 triple4) -> (rule7 % int2)) triple4) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
((((triple2 triple4) -> (rule7 % int3)) ((triple1 triple5) -> (rule8 % int2))) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
((((triple2 triple4) -> (rule7 % int3)) ((triple5 triple1) -> (rule6 % int2))) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion is nice.
("lion" "is" "nice" "+")
triple4
((triple1 triple5) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
((triple5 triple1) -> (rule6 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
((triple1 ((triple3) -> (rule3 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((((triple3) -> (rule3 % int2)) triple1) -> (rule6 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((triple1 ((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2)) triple1) -> (rule6 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion is rough.
("lion" "is" "rough" "+")
triple5
((triple3) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((triple4 triple2) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple1 triple4) -> (rule1 % int2))) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((((triple2 triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
((((((triple2 triple4) -> (rule7 % int3)) triple4) -> (rule1 % int2))) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3