Erin is furry. Gary is quiet. Harry is red. Quiet, kind people are round. All furry, quiet people are kind. All quiet people are kind. If Gary is young and Gary is round then Gary is red. Big, round people are young. If Gary is young and Gary is big then Gary is kind. If someone is quiet and kind then they are young. Big people are round.
Erin is furry.
("Erin" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Quiet, kind people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
All furry, quiet people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
All quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If Gary is young and Gary is round then Gary is red.
((("Gary" "is" "young" "+") ("Gary" "is" "round" "+")) -> ("Gary" "is" "red" "+"))
Big, round people are young.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If Gary is young and Gary is big then Gary is kind.
((("Gary" "is" "young" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "kind" "+"))
If someone is quiet and kind then they are young.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Gary is quiet.
True
1
proof
[(triple2)]
("Gary" "is" "quiet" "+")
triple2
Erin is not furry.
False
1
inv-proof
[(triple1)]
("Erin" "is" "furry" "-")
triple1
Gary is kind.
True
2
proof
[(((triple2) -> rule3))]
("Gary" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple2) -> rule3))]
("Gary" "is" "kind" "-")
((triple2) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
True
4
proof
[(((triple2 ((triple2) -> rule3)) -> rule7))]
("Gary" "is" "young" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not young.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule7))]
("Gary" "is" "young" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
True
9
proof
[(((((triple2 ((triple2) -> rule3)) -> rule7) ((triple2 ((triple2) -> rule3)) -> rule1)) -> rule4))]
("Gary" "is" "red" "+")
((((triple2 ((triple2) -> (rule3 % int4))) -> (rule7 % int3)) ((triple2 ((triple2) -> (rule3 % int4))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Gary is not red.
False
9
inv-proof
[(((((triple2 ((triple2) -> rule3)) -> rule7) ((triple2 ((triple2) -> rule3)) -> rule1)) -> rule4))]
("Gary" "is" "red" "-")
((((triple2 ((triple2) -> (rule3 % int4))) -> (rule7 % int3)) ((triple2 ((triple2) -> (rule3 % int4))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "young" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "kind" "+")
Erin is not young.
Unknown
inv-rconc
[@1: Erin is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "young" "-")
Erin is round.
Unknown
rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "round" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Erin is furry.[(triple1)] Gary is quiet.[(triple2)] Harry is red.[(triple3)] @1: Gary is kind.[(((triple2) -> rule3))] @2: Gary is round.[(((triple2 ((triple2) -> rule3)) -> rule1))] Gary is young.[(((triple2 ((triple2) -> rule3)) -> rule7))] @3: Gary is red.[(((((triple2 ((triple2) -> rule3)) -> rule7) ((triple2 ((triple2) -> rule3)) -> rule1)) -> rule4))]
Erin is furry.
("Erin" "is" "furry" "+")
triple1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((triple2 ((triple2) -> (rule3 % int4))) -> (rule7 % int3)) ((triple2 ((triple2) -> (rule3 % int4))) -> (rule1 % int2))) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4