Anne is cold. Anne is quiet. Anne is smart. Anne is white. Dave is cold. Dave is quiet. Dave is smart. Dave is young. Fiona is blue. Fiona is smart. Fiona is white. Harry is blue. Harry is quiet. Harry is smart. Harry is white. Harry is young. If something is white and cold then it is smart. If something is quiet then it is blue. If Harry is cold and Harry is smart then Harry is white.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is white and cold then it is smart.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If Harry is cold and Harry is smart then Harry is white.
((("Harry" "is" "cold" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "white" "+"))
Fiona is blue.
True
1
proof
[(triple9)]
("Fiona" "is" "blue" "+")
triple9
Anne is not white.
False
1
inv-proof
[(triple4)]
("Anne" "is" "white" "-")
triple4
Dave is blue.
True
2
proof
[(((triple6) -> rule2))]
("Dave" "is" "blue" "+")
((triple6) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple6) -> rule2))]
("Dave" "is" "blue" "-")
((triple6) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is cold.[(triple1)] Anne is quiet.[(triple2)] Anne is smart.[(triple3 OR ((triple4 triple1) -> rule1))] Anne is white.[(triple4)] Dave is cold.[(triple5)] Dave is quiet.[(triple6)] Dave is smart.[(triple7)] Dave is young.[(triple8)] Fiona is blue.[(triple9)] Fiona is smart.[(triple10)] Fiona is white.[(triple11)] Harry is blue.[(triple12 OR ((triple13) -> rule2))] Harry is quiet.[(triple13)] Harry is smart.[(triple14)] Harry is white.[(triple15)] Harry is young.[(triple16)] @1: Anne is blue.[(((triple2) -> rule2))] Dave is blue.[(((triple6) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
((triple4 triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple8
Fiona is blue.
("Fiona" "is" "blue" "+")
triple9
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Fiona is white.
("Fiona" "is" "white" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
((triple13) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
Anne is blue.
("Anne" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple6) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1