Charlie is kind. Dave is not furry. Gary is big. Harry is not big. If Dave is not green then Dave is not kind. If Dave is round then Dave is kind. All big, round things are kind. If something is nice and round then it is kind. Kind, big things are not nice. If something is big then it is round.
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Gary is big.
("Gary" "is" "big" "+")
Harry is not big.
("Harry" "is" "big" "-")
If Dave is not green then Dave is not kind.
((("Dave" "is" "green" "~")) -> ("Dave" "is" "kind" "-"))
If Dave is round then Dave is kind.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "kind" "+"))
All big, round things are kind.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something is nice and round then it is kind.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Kind, big things are not nice.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "-"))
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
Gary is big.
True
1
proof
[(triple3)]
("Gary" "is" "big" "+")
triple3
Charlie is not kind.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "kind" "-")
triple1
Gary is round.
True
2
proof
[(((triple3) -> rule6))]
("Gary" "is" "round" "+")
((triple3) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is not round.
False
2
inv-proof
[(((triple3) -> rule6))]
("Gary" "is" "round" "-")
((triple3) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is kind.
True
4
proof
[(((triple3 ((triple3) -> rule6)) -> rule3))]
("Gary" "is" "kind" "+")
((triple3 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not kind.
False
4
inv-proof
[(((triple3 ((triple3) -> rule6)) -> rule3))]
("Gary" "is" "kind" "-")
((triple3 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not nice.
True
6
proof
[(((((triple3 ((triple3) -> rule6)) -> rule3) triple3) -> rule5))]
("Gary" "is" "nice" "-")
((((triple3 ((triple3) -> (rule6 % int3))) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is nice.
False
6
inv-proof
[(((((triple3 ((triple3) -> rule6)) -> rule3) triple3) -> rule5))]
("Gary" "is" "nice" "+")
((((triple3 ((triple3) -> (rule6 % int3))) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "round" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "round" "-")
Dave is kind.
Unknown
rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Dave" "is" "kind" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is kind.[(triple1)] Dave is not furry.[(triple2)] Gary is big.[(triple3)] Harry is not big.[(triple4)] @1: Gary is round.[(((triple3) -> rule6))] @2: Gary is kind.[(((triple3 ((triple3) -> rule6)) -> rule3))] @3: Gary is not nice.[(((((triple3 ((triple3) -> rule6)) -> rule3) triple3) -> rule5))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Dave is not furry.
("Dave" "is" "furry" "-")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Harry is not big.
("Harry" "is" "big" "-")
triple4
Gary is round.
("Gary" "is" "round" "+")
((triple3) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple3 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is not nice.
("Gary" "is" "nice" "-")
((((triple3 ((triple3) -> (rule6 % int3))) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3