Bob is young. Dave is not green. Gary is red. Harry is white. All big, round things are not green. If Harry is green then Harry is white. If Gary is white then Gary is green. All white things are not round. All green, round things are big. If something is red then it is rough. If Gary is red and Gary is young then Gary is round. If something is rough then it is young.
Bob is young.
("Bob" "is" "young" "+")
Dave is not green.
("Dave" "is" "green" "-")
Gary is red.
("Gary" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
All big, round things are not green.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "-"))
If Harry is green then Harry is white.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "white" "+"))
If Gary is white then Gary is green.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "green" "+"))
All white things are not round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "-"))
All green, round things are big.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If Gary is red and Gary is young then Gary is round.
((("Gary" "is" "red" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "round" "+"))
If something is rough then it is young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Harry is white.
True
1
proof
[(triple4)]
("Harry" "is" "white" "+")
triple4
Harry is not white.
False
1
inv-proof
[(triple4)]
("Harry" "is" "white" "-")
triple4
Gary is rough.
True
2
proof
[(((triple3) -> rule6))]
("Gary" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is round.
False
2
inv-proof
[(((triple4) -> rule4))]
("Harry" "is" "round" "+")
((triple4) -> (rule4 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "rough" "-")
Gary is big.
Unknown
rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Gary" "is" "big" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is young.[(triple1)] Dave is not green.[(triple2)] Gary is red.[(triple3)] Harry is white.[(triple4)] @1: Gary is rough.[(((triple3) -> rule6))] Harry is not round.[(((triple4) -> rule4))] @2: Gary is young.[(((((triple3) -> rule6)) -> rule8))] @3: Gary is round.[(((triple3 ((((triple3) -> rule6)) -> rule8)) -> rule7))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Dave is not green.
("Dave" "is" "green" "-")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Harry is not round.
("Harry" "is" "round" "-")
((triple4) -> (rule4 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule8 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple3 ((((triple3) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3