Dave is round. Dave is smart. Erin is cold. Gary is green. Gary is white. Harry is cold. Harry is white. If Harry is smart and Harry is green then Harry is white. All white people are round. If someone is round and cold then they are green.
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is white.
("Harry" "is" "white" "+")
If Harry is smart and Harry is green then Harry is white.
((("Harry" "is" "smart" "+") ("Harry" "is" "green" "+")) -> ("Harry" "is" "white" "+"))
All white people are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If someone is round and cold then they are green.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
Harry is white.
True
1
proof
[(triple7)]
("Harry" "is" "white" "+")
triple7
Dave is not smart.
False
1
inv-proof
[(triple2)]
("Dave" "is" "smart" "-")
triple2
Harry is round.
True
2
proof
[(((triple7) -> rule2))]
("Harry" "is" "round" "+")
((triple7) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple7) -> rule2))]
("Harry" "is" "round" "-")
((triple7) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
True
4
proof
[(((((triple7) -> rule2) triple6) -> rule3))]
("Harry" "is" "green" "+")
((((triple7) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not green.
False
4
inv-proof
[(((((triple7) -> rule2) triple6) -> rule3))]
("Harry" "is" "green" "-")
((((triple7) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "green" "-")
Erin is round.
Unknown
rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "round" "+")
Erin is not green.
Unknown
inv-rconc
[@2: Erin is green.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Erin" "is" "green" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Dave is round.[(triple1)] Dave is smart.[(triple2)] Erin is cold.[(triple3)] Gary is green.[(triple4)] Gary is white.[(triple5)] Harry is cold.[(triple6)] Harry is white.[(triple7)] @1: Gary is round.[(((triple5) -> rule2))] Harry is round.[(((triple7) -> rule2))] @2: Harry is green.[(((((triple7) -> rule2) triple6) -> rule3))]
Dave is round.
("Dave" "is" "round" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple4
Gary is white.
("Gary" "is" "white" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Gary is round.
("Gary" "is" "round" "+")
((triple5) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple7) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((((triple7) -> (rule2 % int2)) triple6) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2