Bob is cold. Bob is rough. Bob is round. Bob is white. Dave is cold. Dave is green. Dave is kind. Dave is red. Dave is rough. Dave is round. Dave is white. Gary is cold. Gary is green. Gary is kind. Gary is rough. Harry is green. If something is rough then it is cold. If something is green then it is rough.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is green.
("Harry" "is" "green" "+")
If something is rough then it is cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is green then it is rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Gary is kind.
True
1
proof
[(triple14)]
("Gary" "is" "kind" "+")
triple14
Bob is not white.
False
1
inv-proof
[(triple4)]
("Bob" "is" "white" "-")
triple4
Harry is rough.
True
2
proof
[(((triple16) -> rule2))]
("Harry" "is" "rough" "+")
((triple16) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple16) -> rule2))]
("Harry" "is" "rough" "-")
((triple16) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is cold.
True
3
proof
[(((((triple16) -> rule2)) -> rule1))]
("Harry" "is" "cold" "+")
((((triple16) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not cold.
False
3
inv-proof
[(((((triple16) -> rule2)) -> rule1))]
("Harry" "is" "cold" "-")
((((triple16) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Bob is cold.[(triple1 OR ((triple2) -> rule1))] Bob is rough.[(triple2)] Bob is round.[(triple3)] Bob is white.[(triple4)] Dave is cold.[(triple5 OR ((triple9) -> rule1) OR ((((triple6) -> rule2)) -> rule1))] Dave is green.[(triple6)] Dave is kind.[(triple7)] Dave is red.[(triple8)] Dave is rough.[(triple9 OR ((triple6) -> rule2))] Dave is round.[(triple10)] Dave is white.[(triple11)] Gary is cold.[(triple12 OR ((triple15) -> rule1) OR ((((triple13) -> rule2)) -> rule1))] Gary is green.[(triple13)] Gary is kind.[(triple14)] Gary is rough.[(triple15 OR ((triple13) -> rule2))] Harry is green.[(triple16)] @1: Harry is rough.[(((triple16) -> rule2))] @2: Harry is cold.[(((((triple16) -> rule2)) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple2) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
((triple9) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple8
Dave is rough.
("Dave" "is" "rough" "+")
triple9
((triple6) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple10
Dave is white.
("Dave" "is" "white" "+")
triple11
Gary is cold.
("Gary" "is" "cold" "+")
triple12
((triple15) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple13
Gary is kind.
("Gary" "is" "kind" "+")
triple14
Gary is rough.
("Gary" "is" "rough" "+")
triple15
((triple13) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple16
Harry is rough.
("Harry" "is" "rough" "+")
((triple16) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple16) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2