Dave is green. Fiona is white. Harry is cold. If Fiona is green then Fiona is rough. If Harry is cold and Harry is kind then Harry is rough. If someone is kind then they are cold. Nice people are rough. All nice people are white. If someone is green and white then they are rough. If someone is red and green then they are kind. If Dave is green then Dave is red.
Dave is green.
("Dave" "is" "green" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is cold.
("Harry" "is" "cold" "+")
If Fiona is green then Fiona is rough.
((("Fiona" "is" "green" "+")) -> ("Fiona" "is" "rough" "+"))
If Harry is cold and Harry is kind then Harry is rough.
((("Harry" "is" "cold" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "rough" "+"))
If someone is kind then they are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
All nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If someone is green and white then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If someone is red and green then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If Dave is green then Dave is red.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "red" "+"))
Fiona is white.
True
1
proof
[(triple2)]
("Fiona" "is" "white" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple3)]
("Harry" "is" "cold" "-")
triple3
Dave is red.
True
2
proof
[(((triple1) -> rule8))]
("Dave" "is" "red" "+")
((triple1) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple1) -> rule8))]
("Dave" "is" "red" "-")
((triple1) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
True
4
proof
[(((((triple1) -> rule8) triple1) -> rule7))]
("Dave" "is" "kind" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not kind.
False
4
inv-proof
[(((((triple1) -> rule8) triple1) -> rule7))]
("Dave" "is" "kind" "-")
((((triple1) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is cold.
True
5
proof
[(((((((triple1) -> rule8) triple1) -> rule7)) -> rule3))]
("Dave" "is" "cold" "+")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is not cold.
False
5
inv-proof
[(((((((triple1) -> rule8) triple1) -> rule7)) -> rule3))]
("Dave" "is" "cold" "-")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Fiona is not kind.
Unknown
inv-rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "kind" "-")
Harry is rough.
Unknown
rconc
[@2: Harry is rough.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("Harry" "is" "rough" "+")
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Harry" "is" "kind" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "white" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
@0: Dave is green.[(triple1)] Fiona is white.[(triple2)] Harry is cold.[(triple3)] @1: Dave is red.[(((triple1) -> rule8))] @2: Dave is kind.[(((((triple1) -> rule8) triple1) -> rule7))] @3: Dave is cold.[(((((((triple1) -> rule8) triple1) -> rule7)) -> rule3))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Fiona is white.
("Fiona" "is" "white" "+")
triple2
Harry is cold.
("Harry" "is" "cold" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
((triple1) -> (rule8 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule7 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3