Bob is smart. Dave is blue. Erin is cold. Harry is kind. All white things are cold. If something is kind then it is white.
Bob is smart.
("Bob" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All white things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If something is kind then it is white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Harry is kind.
True
1
proof
[(triple4)]
("Harry" "is" "kind" "+")
triple4
Dave is not blue.
False
1
inv-proof
[(triple2)]
("Dave" "is" "blue" "-")
triple2
Harry is white.
True
2
proof
[(((triple4) -> rule2))]
("Harry" "is" "white" "+")
((triple4) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple4) -> rule2))]
("Harry" "is" "white" "-")
((triple4) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
True
3
proof
[(((((triple4) -> rule2)) -> rule1))]
("Harry" "is" "cold" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not cold.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule1))]
("Harry" "is" "cold" "-")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Bob is not cold.
Unknown
inv-rconc
[@2: Bob is cold.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "white" "+")
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Bob is smart.[(triple1)] Dave is blue.[(triple2)] Erin is cold.[(triple3)] Harry is kind.[(triple4)] @1: Harry is white.[(((triple4) -> rule2))] @2: Harry is cold.[(((((triple4) -> rule2)) -> rule1))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2