The bear is big. The bear is green. The bear is nice. If something is green then it is nice. If something is young and nice then it is green. If something is nice then it is green. If something is cold and big then it is green. All young things are green. All big things are green. If the bear is cold and the bear is not young then the bear is big. All young things are big.
The bear is big.
("bear" "is" "big" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is nice.
("bear" "is" "nice" "+")
If something is green then it is nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is young and nice then it is green.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is cold and big then it is green.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
All young things are green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If the bear is cold and the bear is not young then the bear is big.
((("bear" "is" "cold" "+") ("bear" "is" "young" "~")) -> ("bear" "is" "big" "+"))
All young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
The bear is nice.
True
1
proof
[(triple3 OR ((triple2) -> rule1) OR ((((triple1) -> rule6)) -> rule1))]
("bear" "is" "nice" "+")
triple3
((triple2) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The bear is not nice.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule1) OR ((((triple1) -> rule6)) -> rule1))]
("bear" "is" "nice" "-")
triple3
((triple2) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The bear is not young.
Unknown
inv-random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bear is big.[(triple1)] The bear is green.[(triple2 OR ((triple1) -> rule6) OR ((triple3) -> rule3))] The bear is nice.[(triple3 OR ((triple2) -> rule1) OR ((((triple1) -> rule6)) -> rule1))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is green.
("bear" "is" "green" "+")
triple2
((triple1) -> (rule6 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
((triple3) -> (rule3 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
triple3
((triple2) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2