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