Anne is white. Dave is green. Erin is furry. Harry is big. If something is furry then it is cold. Green things are rough. All rough things are furry.
Anne is white.
("Anne" "is" "white" "+")
Dave is green.
("Dave" "is" "green" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Harry is big.
("Harry" "is" "big" "+")
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
All rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
Dave is green.
True
1
proof
[(triple2)]
("Dave" "is" "green" "+")
triple2
Dave is not green.
False
1
inv-proof
[(triple2)]
("Dave" "is" "green" "-")
triple2
Erin is cold.
True
2
proof
[(((triple3) -> rule1))]
("Erin" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "rough" "-")
((triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
True
3
proof
[(((((triple2) -> rule2)) -> rule3))]
("Dave" "is" "furry" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not furry.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("Dave" "is" "furry" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
True
4
proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule1))]
("Dave" "is" "cold" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not cold.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule3)) -> rule1))]
("Dave" "is" "cold" "-")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Anne is not cold.
Unknown
inv-rconc
[@3: Anne is cold.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- FAIL)]]
("Anne" "is" "cold" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "rough" "+")
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "rough" "-")
Harry is furry.
Unknown
rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Harry" "is" "furry" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is white.[(triple1)] Dave is green.[(triple2)] Erin is furry.[(triple3)] Harry is big.[(triple4)] @1: Dave is rough.[(((triple2) -> rule2))] Erin is cold.[(((triple3) -> rule1))] @2: Dave is furry.[(((((triple2) -> rule2)) -> rule3))] @3: Dave is cold.[(((((((triple2) -> rule2)) -> rule3)) -> rule1))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
((triple2) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple3) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple2) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3