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