Bob is red. Bob is round. Dave is cold. Dave is kind. Erin is cold. Gary is round. Gary is white. If something is white then it is round. If something is red and cold then it is not kind. All green, round things are red.
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
If something is white then it is round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
If something is red and cold then it is not kind.
((("something" "is" "red" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "-"))
All green, round things are red.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Erin is cold.
True
1
proof
[(triple5)]
("Erin" "is" "cold" "+")
triple5
Gary is not round.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule1))]
("Gary" "is" "round" "-")
triple6
((triple7) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Bob is red.[(triple1)] Bob is round.[(triple2)] Dave is cold.[(triple3)] Dave is kind.[(triple4)] Erin is cold.[(triple5)] Gary is round.[(triple6 OR ((triple7) -> rule1))] Gary is white.[(triple7)]
Bob is red.
("Bob" "is" "red" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Dave is cold.
("Dave" "is" "cold" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Erin is cold.
("Erin" "is" "cold" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
((triple7) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple7