Bob is quiet. Dave is not cold. Dave is not quiet. If someone is smart then they are not rough. All quiet, young people are rough. If Dave is quiet and Dave is smart then Dave is not young. Quiet people are kind. If someone is quiet and kind then they are cold. If someone is smart and not young then they are cold. Rough, young people are green. If someone is smart and not kind then they are green.
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is not quiet.
("Dave" "is" "quiet" "-")
If someone is smart then they are not rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "-"))
All quiet, young people are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If Dave is quiet and Dave is smart then Dave is not young.
((("Dave" "is" "quiet" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "young" "-"))
Quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If someone is quiet and kind then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is smart and not young then they are cold.
((("someone" "is" "smart" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "cold" "+"))
Rough, young people are green.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone is smart and not kind then they are green.
((("someone" "is" "smart" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "green" "+"))
Dave is not quiet.
True
1
proof
[(triple3)]
("Dave" "is" "quiet" "-")
triple3
Dave is cold.
False
1
inv-proof
[(triple2)]
("Dave" "is" "cold" "+")
triple2
Bob is kind.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "kind" "-")
((triple1) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not smart.
Unknown
inv-random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Bob is quiet.[(triple1)] Dave is not cold.[(triple2)] Dave is not quiet.[(triple3)] @1: Bob is kind.[(((triple1) -> rule4))] @2: Bob is cold.[(((triple1 ((triple1) -> rule4)) -> rule5))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Dave is not cold.
("Dave" "is" "cold" "-")
triple2
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
((triple1) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2