Bob is cold. Bob is not furry. Bob is smart. Bob is not white. Dave is kind. Dave is smart. Dave is young. All smart people are quiet. All smart people are quiet. Quiet, kind people are cold. If someone is quiet and furry then they are not kind. Furry, smart people are not young. If Bob is kind then Bob is cold. If Bob is furry and Bob is not quiet then Bob is cold. If someone is kind and not cold then they are not white.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is not white.
("Bob" "is" "white" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
All smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
All smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Quiet, kind people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is quiet and furry then they are not kind.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "-"))
Furry, smart people are not young.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "-"))
If Bob is kind then Bob is cold.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "cold" "+"))
If Bob is furry and Bob is not quiet then Bob is cold.
((("Bob" "is" "furry" "+") ("Bob" "is" "quiet" "~")) -> ("Bob" "is" "cold" "+"))
If someone is kind and not cold then they are not white.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "white" "-"))
Bob is not white.
True
1
proof
[(triple4)]
("Bob" "is" "white" "-")
triple4
Bob is not smart.
False
1
inv-proof
[(triple3)]
("Bob" "is" "smart" "-")
triple3
Bob is quiet.
True
2
proof
[(((triple3) -> rule1) OR ((triple3) -> rule2))]
("Bob" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple6) -> rule1) OR ((triple6) -> rule2))]
("Dave" "is" "quiet" "-")
((triple6) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple6) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
True
4
proof
[(((((triple6) -> rule1) triple5) -> rule3) OR ((((triple6) -> rule2) triple5) -> rule3))]
("Dave" "is" "cold" "+")
((((triple6) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple6) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not cold.
False
4
inv-proof
[(((((triple6) -> rule1) triple5) -> rule3) OR ((((triple6) -> rule2) triple5) -> rule3))]
("Dave" "is" "cold" "-")
((((triple6) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple6) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is cold.[(triple1)] Bob is not furry.[(triple2)] Bob is not white.[(triple4)] Bob is smart.[(triple3)] Dave is kind.[(triple5)] Dave is smart.[(triple6)] Dave is young.[(triple7)] @1: Bob is quiet.[(((triple3) -> rule1) OR ((triple3) -> rule2))] Dave is quiet.[(((triple6) -> rule1) OR ((triple6) -> rule2))] @2: Dave is cold.[(((((triple6) -> rule1) triple5) -> rule3) OR ((((triple6) -> rule2) triple5) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is not furry.
("Bob" "is" "furry" "-")
triple2
Bob is not white.
("Bob" "is" "white" "-")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple3) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple6) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple6) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple6) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple6) -> (rule2 % int2)) triple5) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2