Bob is cold. Bob is red. Charlie is not blue. Charlie is nice. Charlie is quiet. Charlie is smart. Gary is blue. Gary is nice. Gary is smart. Harry is nice. If Harry is nice then Harry is not rough.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If Harry is nice then Harry is not rough.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "rough" "-"))
Charlie is not blue.
True
1
proof
[(triple3)]
("Charlie" "is" "blue" "-")
triple3
Bob is not red.
False
1
inv-proof
[(triple2)]
("Bob" "is" "red" "-")
triple2
Harry is not rough.
True
2
proof
[(((triple10) -> rule1))]
("Harry" "is" "rough" "-")
((triple10) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is rough.
False
2
inv-proof
[(((triple10) -> rule1))]
("Harry" "is" "rough" "+")
((triple10) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is cold.[(triple1)] Bob is red.[(triple2)] Charlie is nice.[(triple4)] Charlie is not blue.[(triple3)] Charlie is quiet.[(triple5)] Charlie is smart.[(triple6)] Gary is blue.[(triple7)] Gary is nice.[(triple8)] Gary is smart.[(triple9)] Harry is nice.[(triple10)] @1: Harry is not rough.[(((triple10) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Harry is not rough.
("Harry" "is" "rough" "-")
((triple10) -> (rule1 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1