Anne is round. Charlie is round. Gary is quiet. Harry is round. If something is quiet and red then it is young. Furry, kind things are young. Round things are quiet. If something is white then it is young. If something is furry and quiet then it is round. Round things are young. Quiet things are kind. If Gary is round and Gary is young then Gary is red.
Anne is round.
("Anne" "is" "round" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is quiet and red then it is young.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
Furry, kind things are young.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Round things are quiet.
((("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If something is white then it is young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If something is furry and quiet then it is round.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
Round things are young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
Quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If Gary is round and Gary is young then Gary is red.
((("Gary" "is" "round" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "red" "+"))
Anne is round.
True
1
proof
[(triple1)]
("Anne" "is" "round" "+")
triple1
Harry is not round.
False
1
inv-proof
[(triple4)]
("Harry" "is" "round" "-")
triple4
Charlie is young.
True
2
proof
[(((triple2) -> rule6))]
("Charlie" "is" "young" "+")
((triple2) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple4) -> rule3))]
("Harry" "is" "quiet" "-")
((triple4) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Charlie is kind.
True
3
proof
[(((((triple2) -> rule3)) -> rule7))]
("Charlie" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Harry is not kind.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule7))]
("Harry" "is" "kind" "-")
((((triple4) -> (rule3 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Gary is not red.
Unknown
inv-rconc
[@2: Gary is red.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "round" "+")
Gary is not young.
Unknown
inv-rconc
[@3: Gary is young.[CWA. Example of deepest failure = (rule1 <- rule8 <- rule5 <- FAIL)]]
("Gary" "is" "young" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is round.[(triple1)] Charlie is round.[(triple2)] Gary is quiet.[(triple3)] Harry is round.[(triple4)] @1: Anne is quiet.[(((triple1) -> rule3))] Anne is young.[(((triple1) -> rule6))] Charlie is quiet.[(((triple2) -> rule3))] Charlie is young.[(((triple2) -> rule6))] Gary is kind.[(((triple3) -> rule7))] Harry is quiet.[(((triple4) -> rule3))] Harry is young.[(((triple4) -> rule6))] @2: Anne is kind.[(((((triple1) -> rule3)) -> rule7))] Charlie is kind.[(((((triple2) -> rule3)) -> rule7))] Harry is kind.[(((((triple4) -> rule3)) -> rule7))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple2) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple3) -> (rule7 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple4) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule7 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple4) -> (rule3 % int2))) -> (rule7 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2