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