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