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