Anne is blue. Bob is cold. Erin is cold. Harry is blue. If someone is smart then they are blue. If Anne is furry then Anne is white. All smart, cold people are furry. All cold people are blue. If Erin is furry then Erin is rough. Blue people are furry. If Erin is furry and Erin is rough then Erin is smart. All smart, round people are white.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If someone is smart then they are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If Anne is furry then Anne is white.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "white" "+"))
All smart, cold people are furry.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
All cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
If Erin is furry then Erin is rough.
((("Erin" "is" "furry" "+")) -> ("Erin" "is" "rough" "+"))
Blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If Erin is furry and Erin is rough then Erin is smart.
((("Erin" "is" "furry" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "smart" "+"))
All smart, round people are white.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Harry is not blue.
False
1
inv-proof
[(triple4)]
("Harry" "is" "blue" "-")
triple4
Bob is blue.
True
2
proof
[(((triple2) -> rule4))]
("Bob" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple4) -> rule6))]
("Harry" "is" "furry" "-")
((triple4) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule6)) -> rule2))]
("Anne" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not white.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule2))]
("Anne" "is" "white" "-")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Erin is rough.
True
4
proof
[(((((((triple3) -> rule4)) -> rule6)) -> rule5))]
("Erin" "is" "rough" "+")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not rough.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule6)) -> rule5))]
("Erin" "is" "rough" "-")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "white" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "white" "+")
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "white" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is blue.[(triple1)] Bob is cold.[(triple2)] Erin is cold.[(triple3)] Harry is blue.[(triple4)] @1: Anne is furry.[(((triple1) -> rule6))] Bob is blue.[(((triple2) -> rule4))] Erin is blue.[(((triple3) -> rule4))] Harry is furry.[(((triple4) -> rule6))] @2: Anne is white.[(((((triple1) -> rule6)) -> rule2))] Bob is furry.[(((((triple2) -> rule4)) -> rule6))] Erin is furry.[(((((triple3) -> rule4)) -> rule6))] @3: Erin is rough.[(((((((triple3) -> rule4)) -> rule6)) -> rule5))] @4: Erin is smart.[(((((((triple3) -> rule4)) -> rule6) ((((((triple3) -> rule4)) -> rule6)) -> rule5)) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple3) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple4) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((triple2) -> (rule4 % int2))) -> (rule6 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple3) -> (rule4 % int4))) -> (rule6 % int3)) ((((((triple3) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4