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