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