The bear is cold. The bear is green. The bear is nice. The bear is red. The bear is young. If someone is nice then they are green. All young, green people are cold. Green, young people are nice. If the bear is cold then the bear is nice. If someone is nice and not cold then they are red. All green people are red.
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is young.
("bear" "is" "young" "+")
If someone is nice then they are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
All young, green people are cold.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
Green, young people are nice.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If the bear is cold then the bear is nice.
((("bear" "is" "cold" "+")) -> ("bear" "is" "nice" "+"))
If someone is nice and not cold then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "red" "+"))
All green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
The bear is nice.
True
1
proof
[(triple3 OR ((triple1) -> rule4) OR ((triple2 triple5) -> rule3) OR ((((triple5 triple2) -> rule2)) -> rule4))]
("bear" "is" "nice" "+")
triple3
((triple1) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((triple2 triple5) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((((triple5 triple2) -> (rule2 % int2))) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is not young.
False
1
inv-proof
[(triple5)]
("bear" "is" "young" "-")
triple5
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear is cold.[(triple1 OR ((triple5 triple2) -> rule2) OR ((triple5 ((triple3) -> rule1)) -> rule2))] The bear is green.[(triple2 OR ((triple3) -> rule1) OR ((((triple1) -> rule4)) -> rule1))] The bear is nice.[(triple3 OR ((triple1) -> rule4) OR ((triple2 triple5) -> rule3) OR ((((triple5 triple2) -> rule2)) -> rule4))] The bear is red.[(triple4 OR ((triple2) -> rule6) OR ((((triple3) -> rule1)) -> rule6) OR ((((((triple1) -> rule4)) -> rule1)) -> rule6))] The bear is young.[(triple5)]
The bear is cold.
("bear" "is" "cold" "+")
triple1
((triple5 triple2) -> (rule2 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
((triple5 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The bear is green.
("bear" "is" "green" "+")
triple2
((triple3) -> (rule1 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
triple3
((triple1) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((triple2 triple5) -> (rule3 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
((((triple5 triple2) -> (rule2 % int2))) -> (rule4 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The bear is red.
("bear" "is" "red" "+")
triple4
((triple2) -> (rule6 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is green.
("bear" "is" "green" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear is young.
("bear" "is" "young" "+")
triple5