Bob is nice. Harry is cold. If Bob is smart and Bob is not kind then Bob is nice. If Bob is nice then Bob is not white. Smart people are not cold.
Bob is nice.
("Bob" "is" "nice" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If Bob is smart and Bob is not kind then Bob is nice.
((("Bob" "is" "smart" "+") ("Bob" "is" "kind" "~")) -> ("Bob" "is" "nice" "+"))
If Bob is nice then Bob is not white.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "white" "-"))
Smart people are not cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "-"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Harry is not cold.
False
1
inv-proof
[(triple2)]
("Harry" "is" "cold" "-")
triple2
Bob is not white.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "white" "-")
((triple1) -> (rule2 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is white.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "white" "+")
((triple1) -> (rule2 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is nice.[(triple1)] Harry is cold.[(triple2)] @1: Bob is not white.[(((triple1) -> rule2))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Bob is not white.
("Bob" "is" "white" "-")
((triple1) -> (rule2 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1