Dave is blue. Dave is cold. Dave is kind. Dave is nice. Dave is rough. Dave is white. Fiona is not blue. Fiona is cold. Fiona is green. Fiona is kind. Fiona is rough. Harry is blue. Harry is cold. Harry is nice. Harry is white. If something is blue and nice then it is white. If Harry is cold then Harry is green. White things are cold.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is not blue.
("Fiona" "is" "blue" "-")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is blue and nice then it is white.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If Harry is cold then Harry is green.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "green" "+"))
White things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Fiona is green.
True
1
proof
[(triple9)]
("Fiona" "is" "green" "+")
triple9
Harry is not white.
False
1
inv-proof
[(triple15 OR ((triple12 triple14) -> rule1))]
("Harry" "is" "white" "-")
triple15
((triple12 triple14) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "white" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Dave is blue.[(triple1)] Dave is cold.[(triple2 OR ((triple6) -> rule3) OR ((((triple1 triple4) -> rule1)) -> rule3))] Dave is kind.[(triple3)] Dave is nice.[(triple4)] Dave is rough.[(triple5)] Dave is white.[(triple6 OR ((triple1 triple4) -> rule1))] Fiona is cold.[(triple8)] Fiona is green.[(triple9)] Fiona is kind.[(triple10)] Fiona is not blue.[(triple7)] Fiona is rough.[(triple11)] Harry is blue.[(triple12)] Harry is cold.[(triple13 OR ((triple15) -> rule3) OR ((((triple12 triple14) -> rule1)) -> rule3))] Harry is nice.[(triple14)] Harry is white.[(triple15 OR ((triple12 triple14) -> rule1))] @1: Harry is green.[(((triple13) -> rule2) OR ((((triple15) -> rule3)) -> rule2) OR ((((((triple12 triple14) -> rule1)) -> rule3)) -> rule2))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
((triple6) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((((triple1 triple4) -> (rule1 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple1 triple4) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple8
Fiona is green.
("Fiona" "is" "green" "+")
triple9
Fiona is kind.
("Fiona" "is" "kind" "+")
triple10
Fiona is not blue.
("Fiona" "is" "blue" "-")
triple7
Fiona is rough.
("Fiona" "is" "rough" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is cold.
("Harry" "is" "cold" "+")
triple13
((triple15) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple12 triple14) -> (rule1 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
((triple12 triple14) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple13) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple15) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((((triple12 triple14) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3