The bear is kind. If the bear is blue and the bear is not kind then the bear is young. If something is kind then it is young. Kind things are young. If something is big and kind then it is not green. Young things are big. All big things are blue.
The bear is kind.
("bear" "is" "kind" "+")
If the bear is blue and the bear is not kind then the bear is young.
((("bear" "is" "blue" "+") ("bear" "is" "kind" "~")) -> ("bear" "is" "young" "+"))
If something is kind then it is young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is big and kind then it is not green.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "-"))
Young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
The bear is kind.
True
1
proof
[(triple1)]
("bear" "is" "kind" "+")
triple1
The bear is not kind.
False
1
inv-proof
[(triple1)]
("bear" "is" "kind" "-")
triple1
The bear is young.
True
2
proof
[(((triple1) -> rule2) OR ((triple1) -> rule3))]
("bear" "is" "young" "+")
((triple1) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
((triple1) -> (rule3 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is not young.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple1) -> rule3))]
("bear" "is" "young" "-")
((triple1) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
((triple1) -> (rule3 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is big.
True
3
proof
[(((((triple1) -> rule2)) -> rule5) OR ((((triple1) -> rule3)) -> rule5))]
("bear" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is not big.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule5) OR ((((triple1) -> rule3)) -> rule5))]
("bear" "is" "big" "-")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is blue.
True
4
proof
[(((((((triple1) -> rule2)) -> rule5)) -> rule6) OR ((((((triple1) -> rule3)) -> rule5)) -> rule6))]
("bear" "is" "blue" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear is not blue.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule5)) -> rule6) OR ((((((triple1) -> rule3)) -> rule5)) -> rule6))]
("bear" "is" "blue" "-")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
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 kind.[(triple1)] @1: The bear is young.[(((triple1) -> rule2) OR ((triple1) -> rule3))] @2: The bear is big.[(((((triple1) -> rule2)) -> rule5) OR ((((triple1) -> rule3)) -> rule5))] @3: The bear is blue.[(((((((triple1) -> rule2)) -> rule5)) -> rule6) OR ((((((triple1) -> rule3)) -> rule5)) -> rule6))] The bear is not green.[(((((((triple1) -> rule2)) -> rule5) triple1) -> rule4) OR ((((((triple1) -> rule3)) -> rule5) triple1) -> rule4))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
((triple1) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
((triple1) -> (rule3 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is big.
("bear" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear is not green.
("bear" "is" "green" "-")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2)) triple1) -> (rule4 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
((((((triple1) -> (rule3 % int3))) -> (rule5 % int2)) triple1) -> (rule4 % int1))
The bear is not green.
("bear" "is" "green" "-")
int1
The bear is big.
("bear" "is" "big" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3