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