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