Bob is furry. Dave is kind. Erin is furry. Gary is not red. Quiet, big things are furry. Kind, quiet things are furry. If Dave is big and Dave is not round then Dave is kind. If something is kind then it is big. If something is big then it is quiet. If Bob is big and Bob is not cold then Bob is red. If Erin is red and Erin is furry then Erin is kind. If something is red then it is kind.
Bob is furry.
("Bob" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Gary is not red.
("Gary" "is" "red" "-")
Quiet, big things are furry.
((("something" "is" "quiet" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Kind, quiet things are furry.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If Dave is big and Dave is not round then Dave is kind.
((("Dave" "is" "big" "+") ("Dave" "is" "round" "~")) -> ("Dave" "is" "kind" "+"))
If something is kind then it is big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If Bob is big and Bob is not cold then Bob is red.
((("Bob" "is" "big" "+") ("Bob" "is" "cold" "~")) -> ("Bob" "is" "red" "+"))
If Erin is red and Erin is furry then Erin is kind.
((("Erin" "is" "red" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "kind" "+"))
If something is red then it is kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Gary is not red.
True
1
proof
[(triple4)]
("Gary" "is" "red" "-")
triple4
Erin is not furry.
False
1
inv-proof
[(triple3)]
("Erin" "is" "furry" "-")
triple3
Dave is big.
True
2
proof
[(((triple2) -> rule4))]
("Dave" "is" "big" "+")
((triple2) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple2) -> rule4))]
("Dave" "is" "big" "-")
((triple2) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("Dave" "is" "quiet" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not quiet.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("Dave" "is" "quiet" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
True
5
proof
[(((triple2 ((((triple2) -> rule4)) -> rule5)) -> rule2) OR ((((((triple2) -> rule4)) -> rule5) ((triple2) -> rule4)) -> rule1))]
("Dave" "is" "furry" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) ((triple2) -> (rule4 % int3))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not furry.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule4)) -> rule5)) -> rule2) OR ((((((triple2) -> rule4)) -> rule5) ((triple2) -> rule4)) -> rule1))]
("Dave" "is" "furry" "-")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) ((triple2) -> (rule4 % int3))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Bob is not kind.
Unknown
inv-rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("Bob" "is" "kind" "-")
Gary is quiet.
Unknown
rconc
[@3: Gary is quiet.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule8 <- FAIL)]]
("Gary" "is" "quiet" "+")
Gary is not big.
Unknown
inv-rconc
[@2: Gary is big.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Gary" "is" "big" "-")
Bob is quiet.
Unknown
rconc
[@4: Bob is quiet.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule8 <- rule6 <- FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Bob is furry.[(triple1)] Dave is kind.[(triple2)] Erin is furry.[(triple3)] Gary is not red.[(triple4)] @1: Dave is big.[(((triple2) -> rule4))] @2: Dave is quiet.[(((((triple2) -> rule4)) -> rule5))] @3: Dave is furry.[(((triple2 ((((triple2) -> rule4)) -> rule5)) -> rule2) OR ((((((triple2) -> rule4)) -> rule5) ((triple2) -> rule4)) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Gary is not red.
("Gary" "is" "red" "-")
triple4
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2)) ((triple2) -> (rule4 % int3))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3