The bear is blue. The bear is kind. The bear is round. If something is round and nice then it is kind. Kind things are round. Nice, blue things are round. Kind, rough things are round. If something is blue and rough then it is round. Round things are blue. All blue things are nice. Round things are rough.
The bear is blue.
("bear" "is" "blue" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is round.
("bear" "is" "round" "+")
If something is round and nice then it is kind.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Nice, blue things are round.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Kind, rough things are round.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is blue and rough then it is round.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
All blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
The bear is blue.
True
1
proof
[(triple1 OR ((triple3) -> rule6) OR ((((triple2) -> rule2)) -> rule6))]
("bear" "is" "blue" "+")
triple1
((triple3) -> (rule6 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is not kind.
False
1
inv-proof
[(triple2 OR ((triple3 ((triple1) -> rule7)) -> rule1) OR ((triple3 ((((triple3) -> rule6)) -> rule7)) -> rule1) OR ((((((triple1) -> rule7) triple1) -> rule3) ((triple1) -> rule7)) -> rule1) OR ((((((triple1) -> rule7) triple1) -> rule3) ((((triple3) -> rule6)) -> rule7)) -> rule1))]
("bear" "is" "kind" "-")
triple2
((triple3 ((triple1) -> (rule7 % int2))) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
((triple3 ((((triple3) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
((((((triple1) -> (rule7 % int3)) triple1) -> (rule3 % int2)) ((triple1) -> (rule7 % int3))) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
((((((triple1) -> (rule7 % int4)) triple1) -> (rule3 % int3)) ((((triple3) -> (rule6 % int2))) -> (rule7 % int4))) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
@0: The bear is blue.[(triple1 OR ((triple3) -> rule6) OR ((((triple2) -> rule2)) -> rule6))] The bear is kind.[(triple2 OR ((triple3 ((triple1) -> rule7)) -> rule1) OR ((triple3 ((((triple3) -> rule6)) -> rule7)) -> rule1) OR ((((((triple1) -> rule7) triple1) -> rule3) ((triple1) -> rule7)) -> rule1) OR ((((((triple1) -> rule7) triple1) -> rule3) ((((triple3) -> rule6)) -> rule7)) -> rule1))] The bear is round.[(triple3 OR ((triple2) -> rule2) OR ((((triple1) -> rule7) triple1) -> rule3))] @1: The bear is nice.[(((triple1) -> rule7) OR ((((triple3) -> rule6)) -> rule7) OR ((((((triple2) -> rule2)) -> rule6)) -> rule7))] The bear is rough.[(((triple3) -> rule8) OR ((((triple2) -> rule2)) -> rule8) OR ((((((triple1) -> rule7) triple1) -> rule3)) -> rule8))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
((triple3) -> (rule6 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
triple2
((triple3 ((triple1) -> (rule7 % int2))) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
((triple3 ((((triple3) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
int3
((((((triple1) -> (rule7 % int3)) triple1) -> (rule3 % int2)) ((triple1) -> (rule7 % int3))) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
((((((triple1) -> (rule7 % int4)) triple1) -> (rule3 % int3)) ((((triple3) -> (rule6 % int2))) -> (rule7 % int4))) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
int4
The bear is round.
("bear" "is" "round" "+")
triple3
((triple2) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
((((triple1) -> (rule7 % int2)) triple1) -> (rule3 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
((triple1) -> (rule7 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule7 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The bear is rough.
("bear" "is" "rough" "+")
((triple3) -> (rule8 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule8 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
((((((triple1) -> (rule7 % int3)) triple1) -> (rule3 % int2))) -> (rule8 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3