Anne is quiet. Bob is quiet. Fiona is smart. Quiet things are round. If something is kind and young then it is round. If something is round then it is kind. If Fiona is quiet then Fiona is round. All white things are not young. Furry things are young.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If something is kind and young then it is round.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is round then it is kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If Fiona is quiet then Fiona is round.
((("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "round" "+"))
All white things are not young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "-"))
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Bob is quiet.
True
1
proof
[(triple2)]
("Bob" "is" "quiet" "+")
triple2
Fiona is not smart.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "smart" "-")
triple3
Anne is round.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "round" "-")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Anne" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Bob" "is" "kind" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Fiona is not kind.
Unknown
inv-rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "kind" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "young" "+")
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "young" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Anne is quiet.[(triple1)] Bob is quiet.[(triple2)] Fiona is smart.[(triple3)] @1: Anne is round.[(((triple1) -> rule1))] Bob is round.[(((triple2) -> rule1))] @2: Anne is kind.[(((((triple1) -> rule1)) -> rule3))] Bob is kind.[(((((triple2) -> rule1)) -> rule3))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2