Charlie is furry. Charlie is quiet. Charlie is round. Charlie is young. Gary is red. Harry is not furry. Harry is quiet. Harry is red. Harry is round. Harry is white. Round people are nice. If someone is red then they are round. Quiet people are round.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is not furry.
("Harry" "is" "furry" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone is red then they are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Harry is quiet.
True
1
proof
[(triple7)]
("Harry" "is" "quiet" "+")
triple7
Gary is not red.
False
1
inv-proof
[(triple5)]
("Gary" "is" "red" "-")
triple5
Charlie is nice.
True
2
proof
[(((triple3) -> rule1) OR ((((triple2) -> rule3)) -> rule1))]
("Charlie" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Gary is not round.
False
2
inv-proof
[(((triple5) -> rule2))]
("Gary" "is" "round" "-")
((triple5) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
True
3
proof
[(((((triple5) -> rule2)) -> rule1))]
("Gary" "is" "nice" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not nice.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule1))]
("Gary" "is" "nice" "-")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is furry.[(triple1)] Charlie is quiet.[(triple2)] Charlie is round.[(triple3 OR ((triple2) -> rule3))] Charlie is young.[(triple4)] Gary is red.[(triple5)] Harry is not furry.[(triple6)] Harry is quiet.[(triple7)] Harry is red.[(triple8)] Harry is round.[(triple9 OR ((triple7) -> rule3) OR ((triple8) -> rule2))] Harry is white.[(triple10)] @1: Charlie is nice.[(((triple3) -> rule1) OR ((((triple2) -> rule3)) -> rule1))] Gary is round.[(((triple5) -> rule2))] Harry is nice.[(((triple9) -> rule1) OR ((((triple7) -> rule3)) -> rule1) OR ((((triple8) -> rule2)) -> rule1))] @2: Gary is nice.[(((((triple5) -> rule2)) -> rule1))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
((triple2) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Harry is not furry.
("Harry" "is" "furry" "-")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Harry is red.
("Harry" "is" "red" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
((triple7) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((triple8) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple10
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
((triple5) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple9) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2