The bear is big. The bear is cold. The bear is kind. The bear is nice. The bear is round. If someone is nice and round then they are cold. Cold people are round. If the bear is kind and the bear is big then the bear is round. If the bear is nice and the bear is big then the bear is round. If someone is kind then they are nice. If someone is cold then they are kind.
The bear is big.
("bear" "is" "big" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is round.
("bear" "is" "round" "+")
If someone is nice and round then they are cold.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If the bear is kind and the bear is big then the bear is round.
((("bear" "is" "kind" "+") ("bear" "is" "big" "+")) -> ("bear" "is" "round" "+"))
If the bear is nice and the bear is big then the bear is round.
((("bear" "is" "nice" "+") ("bear" "is" "big" "+")) -> ("bear" "is" "round" "+"))
If someone is kind then they are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold then they are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
The bear is nice.
True
1
proof
[(triple4 OR ((triple3) -> rule5) OR ((((triple2) -> rule6)) -> rule5))]
("bear" "is" "nice" "+")
triple4
((triple3) -> (rule5 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bear is not kind.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule6) OR ((((triple4 triple5) -> rule1)) -> rule6) OR ((((triple4 ((triple4 triple1) -> rule4)) -> rule1)) -> rule6))]
("bear" "is" "kind" "-")
triple3
((triple2) -> (rule6 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
((((triple4 triple5) -> (rule1 % int2))) -> (rule6 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
((((triple4 ((triple4 triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
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 cold.[(triple2 OR ((triple4 triple5) -> rule1) OR ((triple4 ((triple3 triple1) -> rule3)) -> rule1) OR ((triple4 ((triple4 triple1) -> rule4)) -> rule1) OR ((((triple3) -> rule5) triple5) -> rule1) OR ((((triple3) -> rule5) ((triple3 triple1) -> rule3)) -> rule1) OR ((((triple3) -> rule5) ((triple4 triple1) -> rule4)) -> rule1) OR ((triple4 ((((triple3) -> rule5) triple1) -> rule4)) -> rule1) OR ((((triple3) -> rule5) ((((triple3) -> rule5) triple1) -> rule4)) -> rule1))] The bear is kind.[(triple3 OR ((triple2) -> rule6) OR ((((triple4 triple5) -> rule1)) -> rule6) OR ((((triple4 ((triple4 triple1) -> rule4)) -> rule1)) -> rule6))] The bear is nice.[(triple4 OR ((triple3) -> rule5) OR ((((triple2) -> rule6)) -> rule5))] The bear is round.[(triple5 OR ((triple2) -> rule2) OR ((triple3 triple1) -> rule3) OR ((triple4 triple1) -> rule4) OR ((((triple2) -> rule6) triple1) -> rule3) OR ((((triple3) -> rule5) triple1) -> rule4) OR ((((((triple2) -> rule6)) -> rule5) triple1) -> rule4))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple2
((triple4 triple5) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
((triple4 ((triple3 triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
((triple4 ((triple4 triple1) -> (rule4 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
((((triple3) -> (rule5 % int2)) triple5) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
((((triple3) -> (rule5 % int3)) ((triple3 triple1) -> (rule3 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
((((triple3) -> (rule5 % int3)) ((triple4 triple1) -> (rule4 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
((triple4 ((((triple3) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
((((triple3) -> (rule5 % int3)) ((((triple3) -> (rule5 % int3)) triple1) -> (rule4 % int2))) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is round.
("bear" "is" "round" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear is kind.
("bear" "is" "kind" "+")
triple3
((triple2) -> (rule6 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
((((triple4 triple5) -> (rule1 % int2))) -> (rule6 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
((((triple4 ((triple4 triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is round.
("bear" "is" "round" "+")
int3
The bear is nice.
("bear" "is" "nice" "+")
triple4
((triple3) -> (rule5 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bear is round.
("bear" "is" "round" "+")
triple5
((triple2) -> (rule2 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
((triple3 triple1) -> (rule3 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
((triple4 triple1) -> (rule4 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
((((triple2) -> (rule6 % int2)) triple1) -> (rule3 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
((((triple3) -> (rule5 % int2)) triple1) -> (rule4 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2)) triple1) -> (rule4 % int1))
The bear is round.
("bear" "is" "round" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
int3