Bob is quiet. Bob is red. Bob is smart. Erin is round. Gary is blue. Gary is furry. Gary is round. If someone is smart and red then they are round. If someone is furry then they are red. All blue, nice people are round. All red, furry people are round. Nice people are smart. Furry, red people are nice. All nice people are furry. All blue people are red.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is round.
("Gary" "is" "round" "+")
If someone is smart and red then they are round.
((("someone" "is" "smart" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is furry then they are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
All blue, nice people are round.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
All red, furry people are round.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
Furry, red people are nice.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
All nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
All blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
Bob is red.
True
1
proof
[(triple2)]
("Bob" "is" "red" "+")
triple2
Erin is not round.
False
1
inv-proof
[(triple4)]
("Erin" "is" "round" "-")
triple4
Bob is round.
True
3
proof
[(((triple3 triple2) -> rule1))]
("Bob" "is" "round" "+")
((triple3 triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple5) -> rule8) OR ((triple6) -> rule2))]
("Gary" "is" "red" "-")
((triple5) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple6) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
True
4
proof
[(((triple6 ((triple5) -> rule8)) -> rule6) OR ((triple6 ((triple6) -> rule2)) -> rule6))]
("Gary" "is" "nice" "+")
((triple6 ((triple5) -> (rule8 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((triple6 ((triple6) -> (rule2 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not nice.
False
4
inv-proof
[(((triple6 ((triple5) -> rule8)) -> rule6) OR ((triple6 ((triple6) -> rule2)) -> rule6))]
("Gary" "is" "nice" "-")
((triple6 ((triple5) -> (rule8 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((triple6 ((triple6) -> (rule2 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Erin is not nice.
Unknown
inv-rconc
[@2: Erin is nice.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is red.
Unknown
rconc
[@3: Erin is red.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule6 <- FAIL)]]
("Erin" "is" "red" "+")
Erin is not furry.
Unknown
inv-rconc
[@2: Erin is furry.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("Erin" "is" "furry" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Bob is quiet.[(triple1)] Bob is red.[(triple2)] Bob is smart.[(triple3)] Erin is round.[(triple4)] Gary is blue.[(triple5)] Gary is furry.[(triple6)] Gary is round.[(triple7 OR ((((triple5) -> rule8) triple6) -> rule4) OR ((((triple6) -> rule2) triple6) -> rule4) OR ((triple5 ((triple6 ((triple5) -> rule8)) -> rule6)) -> rule3) OR ((triple5 ((triple6 ((triple6) -> rule2)) -> rule6)) -> rule3) OR ((((((triple6 ((triple5) -> rule8)) -> rule6)) -> rule5) ((triple5) -> rule8)) -> rule1) OR ((((((triple6 ((triple5) -> rule8)) -> rule6)) -> rule5) ((triple6) -> rule2)) -> rule1) OR ((((((triple6 ((triple6) -> rule2)) -> rule6)) -> rule5) ((triple5) -> rule8)) -> rule1) OR ((((((triple6 ((triple6) -> rule2)) -> rule6)) -> rule5) ((triple6) -> rule2)) -> rule1))] @1: Bob is round.[(((triple3 triple2) -> rule1))] Gary is red.[(((triple5) -> rule8) OR ((triple6) -> rule2))] @2: Gary is nice.[(((triple6 ((triple5) -> rule8)) -> rule6) OR ((triple6 ((triple6) -> rule2)) -> rule6))] @3: Gary is smart.[(((((triple6 ((triple5) -> rule8)) -> rule6)) -> rule5) OR ((((triple6 ((triple6) -> rule2)) -> rule6)) -> rule5))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
((((triple5) -> (rule8 % int2)) triple6) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((((triple6) -> (rule2 % int2)) triple6) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((triple5 ((triple6 ((triple5) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((triple5 ((triple6 ((triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((((triple6 ((triple5) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((triple5) -> (rule8 % int4))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
((((((triple6 ((triple5) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((triple6) -> (rule2 % int4))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
((((((triple6 ((triple6) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((triple5) -> (rule8 % int4))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
((((((triple6 ((triple6) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) ((triple6) -> (rule2 % int4))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Bob is round.
("Bob" "is" "round" "+")
((triple3 triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple5) -> (rule8 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple6) -> (rule2 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple6 ((triple5) -> (rule8 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
((triple6 ((triple6) -> (rule2 % int2))) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple6 ((triple5) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
((((triple6 ((triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3