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