Bob is quiet. Bob is rough. Bob is smart. Bob is young. Charlie is not nice. Erin is cold. Erin is young. If something is cold and not smart then it is not nice. Smart things are not nice. If Bob is not white then Bob is rough. If Bob is cold then Bob is not nice. If Erin is cold and Erin is quiet then Erin is young. All white things are quiet. If something is quiet and not rough then it is young. If something is white then it is young.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is cold and not smart then it is not nice.
((("something" "is" "cold" "+") ("something" "is" "smart" "~")) -> ("something" "is" "nice" "-"))
Smart things are not nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "-"))
If Bob is not white then Bob is rough.
((("Bob" "is" "white" "~")) -> ("Bob" "is" "rough" "+"))
If Bob is cold then Bob is not nice.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "nice" "-"))
If Erin is cold and Erin is quiet then Erin is young.
((("Erin" "is" "cold" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "young" "+"))
All white things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and not rough then it is young.
((("something" "is" "quiet" "+") ("something" "is" "rough" "~")) -> ("something" "is" "young" "+"))
If something is white then it is young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
Bob is quiet.
True
1
proof
[(triple1)]
("Bob" "is" "quiet" "+")
triple1
Bob is not smart.
False
1
inv-proof
[(triple3)]
("Bob" "is" "smart" "-")
triple3
Bob is not nice.
True
2
proof
[(((triple3) -> rule2))]
("Bob" "is" "nice" "-")
((triple3) -> (rule2 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is nice.
False
2
inv-proof
[(((triple3) -> rule2))]
("Bob" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "quiet" "-")
Charlie is young.
Unknown
rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "young" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Bob is quiet.[(triple1)] Bob is rough.[(triple2)] Bob is smart.[(triple3)] Bob is young.[(triple4)] Charlie is not nice.[(triple5)] Erin is cold.[(triple6)] Erin is young.[(triple7)] @1: Bob is not nice.[(((triple3) -> rule2))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Bob is not nice.
("Bob" "is" "nice" "-")
((triple3) -> (rule2 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1