Bob is blue. Bob is not cold. Bob is young. Red, young people are cold. All cold people are blue. Red people are blue. If someone is round and not big then they are green. Round people are not green. If someone is blue and not cold then they are round.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is young.
("Bob" "is" "young" "+")
Red, young people are cold.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
All cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is round and not big then they are green.
((("someone" "is" "round" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "green" "+"))
Round people are not green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "-"))
If someone is blue and not cold then they are round.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "round" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Bob is round.
True
3
proof
[(((triple1 triple2) -> rule6))]
("Bob" "is" "round" "+")
((triple1 triple2) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
3
inv-proof
[(((triple1 triple2) -> rule6))]
("Bob" "is" "round" "-")
((triple1 triple2) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not green.
True
4
proof
[(((((triple1 triple2) -> rule6)) -> rule5))]
("Bob" "is" "green" "-")
((((triple1 triple2) -> (rule6 % int2))) -> (rule5 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is green.
False
4
inv-proof
[(((((triple1 triple2) -> rule6)) -> rule5))]
("Bob" "is" "green" "+")
((((triple1 triple2) -> (rule6 % int2))) -> (rule5 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is blue.[(triple1)] Bob is not cold.[(triple2)] Bob is young.[(triple3)] @1: Bob is round.[(((triple1 triple2) -> rule6))] @2: Bob is not green.[(((((triple1 triple2) -> rule6)) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is not cold.
("Bob" "is" "cold" "-")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
((triple1 triple2) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not green.
("Bob" "is" "green" "-")
((((triple1 triple2) -> (rule6 % int2))) -> (rule5 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2