Anne is cold. Anne is not green. Bob is red. Erin is furry. Harry is cold. Harry is green. Harry is rough. If someone is red then they are furry. If Erin is quiet and Erin is furry then Erin is not red. If someone is white and not rough then they are green. Furry people are green. All quiet, furry people are cold. If someone is white then they are red. All furry, green people are not quiet. If someone is cold then they are quiet.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is not green.
("Anne" "is" "green" "-")
Bob is red.
("Bob" "is" "red" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is red then they are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
If Erin is quiet and Erin is furry then Erin is not red.
((("Erin" "is" "quiet" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "red" "-"))
If someone is white and not rough then they are green.
((("someone" "is" "white" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "green" "+"))
Furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
All quiet, furry people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If someone is white then they are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
All furry, green people are not quiet.
((("someone" "is" "furry" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "-"))
If someone is cold then they are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
Bob is red.
True
1
proof
[(triple3)]
("Bob" "is" "red" "+")
triple3
Erin is not furry.
False
1
inv-proof
[(triple4)]
("Erin" "is" "furry" "-")
triple4
Erin is green.
True
2
proof
[(((triple4) -> rule4))]
("Erin" "is" "green" "+")
((triple4) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple4) -> rule4))]
("Erin" "is" "green" "-")
((triple4) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Bob is green.
True
3
proof
[(((((triple3) -> rule1)) -> rule4))]
("Bob" "is" "green" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Erin is quiet.
False
4
inv-proof
[(((triple4 ((triple4) -> rule4)) -> rule7))]
("Erin" "is" "quiet" "+")
((triple4 ((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Bob is not quiet.
True
6
proof
[(((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule4)) -> rule7))]
("Bob" "is" "quiet" "-")
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is quiet.
False
6
inv-proof
[(((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule4)) -> rule7))]
("Bob" "is" "quiet" "+")
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "cold" "-")
Anne is red.
Unknown
rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "red" "+")
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "red" "-")
Anne is furry.
Unknown
rconc
[@2: Anne is furry.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Anne is cold.[(triple1)] Anne is not green.[(triple2)] Bob is red.[(triple3)] Erin is furry.[(triple4)] Harry is cold.[(triple5)] Harry is green.[(triple6)] Harry is rough.[(triple7)] @1: Anne is quiet.[(((triple1) -> rule8))] Bob is furry.[(((triple3) -> rule1))] Erin is green.[(((triple4) -> rule4))] Harry is quiet.[(((triple5) -> rule8))] @2: Bob is green.[(((((triple3) -> rule1)) -> rule4))] Erin is not quiet.[(((triple4 ((triple4) -> rule4)) -> rule7))] @3: Bob is not quiet.[(((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule4)) -> rule7))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is not green.
("Anne" "is" "green" "-")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule8 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple4) -> (rule4 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple5) -> (rule8 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Erin is not quiet.
("Erin" "is" "quiet" "-")
((triple4 ((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Bob is not quiet.
("Bob" "is" "quiet" "-")
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3