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