Charlie is nice. Charlie is quiet. Gary is not green. Gary is nice. Harry is furry. Harry is nice. Harry is white. If someone is quiet then they are not big. Nice, white people are quiet. If someone is blue and big then they are not nice.
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is quiet then they are not big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "-"))
Nice, white people are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is blue and big then they are not nice.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "-"))
Charlie is quiet.
True
1
proof
[(triple2)]
("Charlie" "is" "quiet" "+")
triple2
Harry is not furry.
False
1
inv-proof
[(triple5)]
("Harry" "is" "furry" "-")
triple5
Charlie is not big.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "big" "-")
((triple2) -> (rule1 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is big.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "big" "+")
((triple2) -> (rule1 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Harry is not big.
True
4
proof
[(((((triple6 triple7) -> rule2)) -> rule1))]
("Harry" "is" "big" "-")
((((triple6 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is big.
False
4
inv-proof
[(((((triple6 triple7) -> rule2)) -> rule1))]
("Harry" "is" "big" "+")
((((triple6 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Charlie is nice.[(triple1)] Charlie is quiet.[(triple2)] Gary is nice.[(triple4)] Gary is not green.[(triple3)] Harry is furry.[(triple5)] Harry is nice.[(triple6)] Harry is white.[(triple7)] @1: Charlie is not big.[(((triple2) -> rule1))] Harry is quiet.[(((triple6 triple7) -> rule2))] @2: Harry is not big.[(((((triple6 triple7) -> rule2)) -> rule1))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Gary is not green.
("Gary" "is" "green" "-")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Charlie is not big.
("Charlie" "is" "big" "-")
((triple2) -> (rule1 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple6 triple7) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not big.
("Harry" "is" "big" "-")
((((triple6 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2