Anne is cold. Anne is nice. Anne is smart. Anne is young. Bob is red. Bob is rough. Bob is young. If Anne is not quiet then Anne is cold. Quiet people are smart. All smart people are red. Quiet people are red. If Bob is red and Bob is rough then Bob is smart. If Bob is not smart then Bob is young. If someone is rough and not red then they are cold. If someone is nice and cold then they are young.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
If Anne is not quiet then Anne is cold.
((("Anne" "is" "quiet" "~")) -> ("Anne" "is" "cold" "+"))
Quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
All smart people are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Quiet people are red.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If Bob is red and Bob is rough then Bob is smart.
((("Bob" "is" "red" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "smart" "+"))
If Bob is not smart then Bob is young.
((("Bob" "is" "smart" "~")) -> ("Bob" "is" "young" "+"))
If someone is rough and not red then they are cold.
((("someone" "is" "rough" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "cold" "+"))
If someone is nice and cold then they are young.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Bob is young.
True
1
proof
[(triple7)]
("Bob" "is" "young" "+")
triple7
Bob is not rough.
False
1
inv-proof
[(triple6)]
("Bob" "is" "rough" "-")
triple6
Anne is red.
True
2
proof
[(((triple3) -> rule3))]
("Anne" "is" "red" "+")
((triple3) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is not smart.
False
3
inv-proof
[(((triple5 triple6) -> rule5))]
("Bob" "is" "smart" "-")
((triple5 triple6) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "cold" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Anne is cold.[(triple1)] Anne is nice.[(triple2)] Anne is smart.[(triple3)] Anne is young.[(triple4 OR ((triple2 triple1) -> rule8))] Bob is red.[(triple5)] Bob is rough.[(triple6)] Bob is young.[(triple7)] @1: Anne is red.[(((triple3) -> rule3))] Bob is smart.[(((triple5 triple6) -> rule5))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
triple4
((triple2 triple1) -> (rule8 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is rough.
("Bob" "is" "rough" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Anne is red.
("Anne" "is" "red" "+")
((triple3) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple5 triple6) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1