Bob is blue. Bob is kind. Bob is quiet. Dave is blue. Dave is cold. Dave is kind. Dave is quiet. If something is blue then it is green. If something is smart and cold then it is kind. Kind, smart things are cold. All blue, green things are cold. Cold, kind things are young. If something is cold and not kind then it is young.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is smart and cold then it is kind.
((("something" "is" "smart" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Kind, smart things are cold.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
All blue, green things are cold.
((("something" "is" "blue" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Cold, kind things are young.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is cold and not kind then it is young.
((("something" "is" "cold" "+") ("something" "is" "kind" "~")) -> ("something" "is" "young" "+"))
Dave is quiet.
True
1
proof
[(triple7)]
("Dave" "is" "quiet" "+")
triple7
Dave is not kind.
False
1
inv-proof
[(triple6)]
("Dave" "is" "kind" "-")
triple6
Dave is young.
True
3
proof
[(((triple5 triple6) -> rule5) OR ((((triple4 ((triple4) -> rule1)) -> rule4) triple6) -> rule5))]
("Dave" "is" "young" "+")
((triple5 triple6) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule4 % int2)) triple6) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "green" "-")
((triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule4))]
("Bob" "is" "cold" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not cold.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule4))]
("Bob" "is" "cold" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
True
6
proof
[(((((triple1 ((triple1) -> rule1)) -> rule4) triple2) -> rule5))]
("Bob" "is" "young" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not young.
False
6
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule4) triple2) -> rule5))]
("Bob" "is" "young" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is blue.[(triple1)] Bob is kind.[(triple2)] Bob is quiet.[(triple3)] Dave is blue.[(triple4)] Dave is cold.[(triple5 OR ((triple4 ((triple4) -> rule1)) -> rule4))] Dave is kind.[(triple6)] Dave is quiet.[(triple7)] @1: Bob is green.[(((triple1) -> rule1))] Dave is green.[(((triple4) -> rule1))] Dave is young.[(((triple5 triple6) -> rule5) OR ((((triple4 ((triple4) -> rule1)) -> rule4) triple6) -> rule5))] @2: Bob is cold.[(((triple1 ((triple1) -> rule1)) -> rule4))] @3: Bob is young.[(((((triple1 ((triple1) -> rule1)) -> rule4) triple2) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
((triple4 ((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple4) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple5 triple6) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple4 ((triple4) -> (rule1 % int3))) -> (rule4 % int2)) triple6) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3