Anne is cold. Anne is green. Anne is quiet. Anne is white. Bob is cold. Bob is green. Bob is quiet. Bob is smart. Bob is young. Dave is nice. Dave is smart. Dave is young. If something is cold then it is nice. All nice, cold things are smart. Young, cold things are nice.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
All nice, cold things are smart.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Young, cold things are nice.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Anne is quiet.
True
1
proof
[(triple3)]
("Anne" "is" "quiet" "+")
triple3
Bob is not cold.
False
1
inv-proof
[(triple5)]
("Bob" "is" "cold" "-")
triple5
Bob is nice.
True
2
proof
[(((triple5) -> rule1) OR ((triple9 triple5) -> rule3))]
("Bob" "is" "nice" "+")
((triple5) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple9 triple5) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "nice" "-")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule2))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not smart.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule2))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2)] Anne is quiet.[(triple3)] Anne is white.[(triple4)] Bob is cold.[(triple5)] Bob is green.[(triple6)] Bob is quiet.[(triple7)] Bob is smart.[(triple8 OR ((((triple5) -> rule1) triple5) -> rule2) OR ((((triple9 triple5) -> rule3) triple5) -> rule2))] Bob is young.[(triple9)] Dave is nice.[(triple10)] Dave is smart.[(triple11)] Dave is young.[(triple12)] @1: Anne is nice.[(((triple1) -> rule1))] Bob is nice.[(((triple5) -> rule1) OR ((triple9 triple5) -> rule3))] @2: Anne is smart.[(((((triple1) -> rule1) triple1) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Bob is cold.
("Bob" "is" "cold" "+")
triple5
Bob is green.
("Bob" "is" "green" "+")
triple6
Bob is quiet.
("Bob" "is" "quiet" "+")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
triple8
((((triple5) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple9 triple5) -> (rule3 % int2)) triple5) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple9
Dave is nice.
("Dave" "is" "nice" "+")
triple10
Dave is smart.
("Dave" "is" "smart" "+")
triple11
Dave is young.
("Dave" "is" "young" "+")
triple12
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple5) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple9 triple5) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2