Dave is blue. Dave is not green. Dave is nice. Dave is smart. Dave is white. Dave is young. Gary is blue. Gary is cold. Gary is green. Gary is white. Harry is blue. Harry is green. Harry is nice. Harry is white. Harry is young. If Harry is cold then Harry is not smart. If something is young then it is not cold. Cold things are green.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is cold then Harry is not smart.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "smart" "-"))
If something is young then it is not cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "-"))
Cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Harry is nice.
True
1
proof
[(triple13)]
("Harry" "is" "nice" "+")
triple13
Dave is not smart.
False
1
inv-proof
[(triple4)]
("Dave" "is" "smart" "-")
triple4
Harry is not cold.
True
2
proof
[(((triple15) -> rule2))]
("Harry" "is" "cold" "-")
((triple15) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is cold.
False
2
inv-proof
[(((triple15) -> rule2))]
("Harry" "is" "cold" "+")
((triple15) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Dave is blue.[(triple1)] Dave is nice.[(triple3)] Dave is not green.[(triple2)] Dave is smart.[(triple4)] Dave is white.[(triple5)] Dave is young.[(triple6)] Gary is blue.[(triple7)] Gary is cold.[(triple8)] Gary is green.[(triple9 OR ((triple8) -> rule3))] Gary is white.[(triple10)] Harry is blue.[(triple11)] Harry is green.[(triple12)] Harry is nice.[(triple13)] Harry is white.[(triple14)] Harry is young.[(triple15)] @1: Dave is not cold.[(((triple6) -> rule2))] Harry is not cold.[(((triple15) -> rule2))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Dave is not green.
("Dave" "is" "green" "-")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is green.
("Gary" "is" "green" "+")
triple9
((triple8) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple10
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is nice.
("Harry" "is" "nice" "+")
triple13
Harry is white.
("Harry" "is" "white" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
Dave is not cold.
("Dave" "is" "cold" "-")
((triple6) -> (rule2 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
((triple15) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1