Charlie is rough. Dave is rough. Gary is rough. Harry is young. If something is young then it is rough. If something is big and white then it is round.
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is young then it is rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If something is big and white then it is round.
((("something" "is" "big" "+") ("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Dave is rough.
True
1
proof
[(triple2)]
("Dave" "is" "rough" "+")
triple2
Harry is not young.
False
1
inv-proof
[(triple4)]
("Harry" "is" "young" "-")
triple4
Harry is rough.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "rough" "+")
((triple4) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple4) -> rule1))]
("Harry" "is" "rough" "-")
((triple4) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "round" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "round" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Charlie is rough.[(triple1)] Dave is rough.[(triple2)] Gary is rough.[(triple3)] Harry is young.[(triple4)] @1: Harry is rough.[(((triple4) -> rule1))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Harry is rough.
("Harry" "is" "rough" "+")
((triple4) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1