Dave is red. Erin is round. Gary is nice. White things are furry. If something is red then it is young. All white, nice things are young. All nice things are red. If Dave is young then Dave is round. If something is nice then it is white. If something is round then it is furry. All white things are round.
Dave is red.
("Dave" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is nice.
("Gary" "is" "nice" "+")
White things are furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If something is red then it is young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All white, nice things are young.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
All nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If Dave is young then Dave is round.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "round" "+"))
If something is nice then it is white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If something is round then it is furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
All white things are round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Dave is red.
True
1
proof
[(triple1)]
("Dave" "is" "red" "+")
triple1
Erin is not round.
False
1
inv-proof
[(triple2)]
("Erin" "is" "round" "-")
triple2
Dave is young.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "young" "+")
((triple1) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple2) -> rule7))]
("Erin" "is" "furry" "-")
((triple2) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Gary is furry.
True
3
proof
[(((((triple3) -> rule6)) -> rule1) OR ((((((triple3) -> rule6)) -> rule8)) -> rule7))]
("Gary" "is" "furry" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((((triple3) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not round.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule8))]
("Gary" "is" "round" "-")
((((triple3) -> (rule6 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Dave is furry.
True
4
proof
[(((((((triple1) -> rule2)) -> rule5)) -> rule7))]
("Dave" "is" "furry" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not furry.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule5)) -> rule7))]
("Dave" "is" "furry" "-")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "white" "-")
Erin is white.
Unknown
rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "white" "+")
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "red" "-")
Erin is young.
Unknown
rconc
[@2: Erin is young.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Erin" "is" "young" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Dave is red.[(triple1)] Erin is round.[(triple2)] Gary is nice.[(triple3)] @1: Dave is young.[(((triple1) -> rule2))] Erin is furry.[(((triple2) -> rule7))] Gary is red.[(((triple3) -> rule4))] Gary is white.[(((triple3) -> rule6))] @2: Dave is round.[(((((triple1) -> rule2)) -> rule5))] Gary is furry.[(((((triple3) -> rule6)) -> rule1) OR ((((((triple3) -> rule6)) -> rule8)) -> rule7))] Gary is round.[(((((triple3) -> rule6)) -> rule8))] Gary is young.[(((((triple3) -> rule4)) -> rule2) OR ((((triple3) -> rule6) triple3) -> rule3))] @3: Dave is furry.[(((((((triple1) -> rule2)) -> rule5)) -> rule7))]
Dave is red.
("Dave" "is" "red" "+")
triple1
Erin is round.
("Erin" "is" "round" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
((triple1) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple2) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple3) -> (rule4 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
((((((triple3) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is round.
("Gary" "is" "round" "+")
((((triple3) -> (rule6 % int2))) -> (rule8 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple3) -> (rule6 % int2)) triple3) -> (rule3 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3