Bob is cold. Bob is green. Bob is quiet. Bob is not red. Bob is rough. Erin is not cold. Erin is quiet. If Bob is cold and Bob is quiet then Bob is kind. Smart, rough things are not quiet. If something is quiet and not cold then it is red.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not red.
("Bob" "is" "red" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
If Bob is cold and Bob is quiet then Bob is kind.
((("Bob" "is" "cold" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "kind" "+"))
Smart, rough things are not quiet.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "-"))
If something is quiet and not cold then it is red.
((("something" "is" "quiet" "+") ("something" "is" "cold" "~")) -> ("something" "is" "red" "+"))
Bob is not red.
True
1
proof
[(triple4)]
("Bob" "is" "red" "-")
triple4
Bob is not quiet.
False
1
inv-proof
[(triple3)]
("Bob" "is" "quiet" "-")
triple3
Erin is red.
True
3
proof
[(((triple7 triple6) -> rule3))]
("Erin" "is" "red" "+")
((triple7 triple6) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not red.
False
3
inv-proof
[(((triple7 triple6) -> rule3))]
("Erin" "is" "red" "-")
((triple7 triple6) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is cold.[(triple1)] Bob is green.[(triple2)] Bob is not red.[(triple4)] Bob is quiet.[(triple3)] Bob is rough.[(triple5)] Erin is not cold.[(triple6)] Erin is quiet.[(triple7)] @1: Bob is kind.[(((triple1 triple3) -> rule1))] Erin is red.[(((triple7 triple6) -> rule3))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is not red.
("Bob" "is" "red" "-")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Erin is not cold.
("Erin" "is" "cold" "-")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
Bob is kind.
("Bob" "is" "kind" "+")
((triple1 triple3) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple7 triple6) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1