Anne is not rough. Dave is not green. Dave is not kind. Dave is round. Dave is young. Gary is green. Gary is kind. Gary is red. Gary is rough. Harry is young. If Anne is green then Anne is red. If Harry is kind and Harry is not red then Harry is green. If someone is rough then they are round. Young, green people are quiet. If someone is green and not round then they are not young. Red, round people are young.
Anne is not rough.
("Anne" "is" "rough" "-")
Dave is not green.
("Dave" "is" "green" "-")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
If Anne is green then Anne is red.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "red" "+"))
If Harry is kind and Harry is not red then Harry is green.
((("Harry" "is" "kind" "+") ("Harry" "is" "red" "~")) -> ("Harry" "is" "green" "+"))
If someone is rough then they are round.
((("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
Young, green people are quiet.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
If someone is green and not round then they are not young.
((("someone" "is" "green" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "young" "-"))
Red, round people are young.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Gary is rough.
True
1
proof
[(triple9)]
("Gary" "is" "rough" "+")
triple9
Gary is not kind.
False
1
inv-proof
[(triple7)]
("Gary" "is" "kind" "-")
triple7
Gary is round.
True
2
proof
[(((triple9) -> rule3))]
("Gary" "is" "round" "+")
((triple9) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is not round.
False
2
inv-proof
[(((triple9) -> rule3))]
("Gary" "is" "round" "-")
((triple9) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is young.
True
4
proof
[(((triple8 ((triple9) -> rule3)) -> rule6))]
("Gary" "is" "young" "+")
((triple8 ((triple9) -> (rule3 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not young.
False
4
inv-proof
[(((triple8 ((triple9) -> rule3)) -> rule6))]
("Gary" "is" "young" "-")
((triple8 ((triple9) -> (rule3 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is quiet.
True
6
proof
[(((((triple8 ((triple9) -> rule3)) -> rule6) triple6) -> rule4))]
("Gary" "is" "quiet" "+")
((((triple8 ((triple9) -> (rule3 % int3))) -> (rule6 % int2)) triple6) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is not quiet.
False
6
inv-proof
[(((((triple8 ((triple9) -> rule3)) -> rule6) triple6) -> rule4))]
("Gary" "is" "quiet" "-")
((((triple8 ((triple9) -> (rule3 % int3))) -> (rule6 % int2)) triple6) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "round" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "round" "+")
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is young.
Unknown
rconc
[@2: Anne is young.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Anne" "is" "young" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is not rough.[(triple1)] Dave is not green.[(triple2)] Dave is not kind.[(triple3)] Dave is round.[(triple4)] Dave is young.[(triple5)] Gary is green.[(triple6)] Gary is kind.[(triple7)] Gary is red.[(triple8)] Gary is rough.[(triple9)] Harry is young.[(triple10)] @1: Gary is round.[(((triple9) -> rule3))] @2: Gary is young.[(((triple8 ((triple9) -> rule3)) -> rule6))] @3: Gary is quiet.[(((((triple8 ((triple9) -> rule3)) -> rule6) triple6) -> rule4))]
Anne is not rough.
("Anne" "is" "rough" "-")
triple1
Dave is not green.
("Dave" "is" "green" "-")
triple2
Dave is not kind.
("Dave" "is" "kind" "-")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Dave is young.
("Dave" "is" "young" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Gary is red.
("Gary" "is" "red" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
((triple9) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple8 ((triple9) -> (rule3 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple8 ((triple9) -> (rule3 % int3))) -> (rule6 % int2)) triple6) -> (rule4 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3