Dave is red. Fiona is not rough. Harry is blue. If someone is cold then they are nice. If someone is smart then they are not nice. All red, rough people are not nice. If someone is red then they are cold. If someone is white then they are blue. If Harry is rough and Harry is not smart then Harry is red.
Dave is red.
("Dave" "is" "red" "+")
Fiona is not rough.
("Fiona" "is" "rough" "-")
Harry is blue.
("Harry" "is" "blue" "+")
If someone is cold then they are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is smart then they are not nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "-"))
All red, rough people are not nice.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "-"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is white then they are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If Harry is rough and Harry is not smart then Harry is red.
((("Harry" "is" "rough" "+") ("Harry" "is" "smart" "~")) -> ("Harry" "is" "red" "+"))
Harry is blue.
True
1
proof
[(triple3)]
("Harry" "is" "blue" "+")
triple3
Dave is not red.
False
1
inv-proof
[(triple1)]
("Dave" "is" "red" "-")
triple1
Dave is cold.
True
2
proof
[(((triple1) -> rule4))]
("Dave" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "cold" "-")
((triple1) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
True
3
proof
[(((((triple1) -> rule4)) -> rule1))]
("Dave" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is not nice.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule1))]
("Dave" "is" "nice" "-")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Harry is not cold.
Unknown
inv-rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Harry" "is" "cold" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "cold" "+")
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Dave is red.[(triple1)] Fiona is not rough.[(triple2)] Harry is blue.[(triple3)] @1: Dave is cold.[(((triple1) -> rule4))] @2: Dave is nice.[(((((triple1) -> rule4)) -> rule1))]
Dave is red.
("Dave" "is" "red" "+")
triple1
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
triple3
Dave is cold.
("Dave" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2