Anne is kind. Anne is not rough. Bob is furry. Fiona is cold. Fiona is quiet. Fiona is rough. Fiona is young. All cold things are quiet. Furry, kind things are quiet. Quiet things are kind. If Fiona is kind then Fiona is furry. All furry things are cold. If something is young and quiet then it is rough. If something is smart then it is rough. If something is young and not quiet then it is rough.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not rough.
("Anne" "is" "rough" "-")
Bob is furry.
("Bob" "is" "furry" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is young.
("Fiona" "is" "young" "+")
All cold things are quiet.
((("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
Furry, kind things are quiet.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
Quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If Fiona is kind then Fiona is furry.
((("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "furry" "+"))
All furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is young and quiet then it is rough.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is smart then it is rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is young and not quiet then it is rough.
((("something" "is" "young" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "rough" "+"))
Fiona is cold.
True
1
proof
[(triple4 OR ((((((triple5) -> rule3)) -> rule4)) -> rule5))]
("Fiona" "is" "cold" "+")
triple4
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Bob is not furry.
False
1
inv-proof
[(triple3)]
("Bob" "is" "furry" "-")
triple3
Bob is cold.
True
2
proof
[(((triple3) -> rule5))]
("Bob" "is" "cold" "+")
((triple3) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple3) -> rule5))]
("Bob" "is" "cold" "-")
((triple3) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Fiona is furry.
True
3
proof
[(((((triple5) -> rule3)) -> rule4) OR ((((((triple4) -> rule1)) -> rule3)) -> rule4))]
("Fiona" "is" "furry" "+")
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Bob is not quiet.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule1))]
("Bob" "is" "quiet" "-")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is kind.
True
4
proof
[(((((((triple3) -> rule5)) -> rule1)) -> rule3))]
("Bob" "is" "kind" "+")
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not kind.
False
4
inv-proof
[(((((((triple3) -> rule5)) -> rule1)) -> rule3))]
("Bob" "is" "kind" "-")
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Anne is not quiet.
Unknown
inv-rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Anne" "is" "quiet" "-")
Anne is cold.
Unknown
rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "cold" "+")
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "rough" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is kind.[(triple1)] Anne is not rough.[(triple2)] Bob is furry.[(triple3)] Fiona is cold.[(triple4 OR ((((((triple5) -> rule3)) -> rule4)) -> rule5))] Fiona is quiet.[(triple5 OR ((triple4) -> rule1))] Fiona is rough.[(triple6 OR ((triple7 triple5) -> rule6) OR ((triple7 ((triple4) -> rule1)) -> rule6))] Fiona is young.[(triple7)] @1: Bob is cold.[(((triple3) -> rule5))] Fiona is kind.[(((triple5) -> rule3) OR ((((triple4) -> rule1)) -> rule3))] @2: Bob is quiet.[(((((triple3) -> rule5)) -> rule1))] Fiona is furry.[(((((triple5) -> rule3)) -> rule4) OR ((((((triple4) -> rule1)) -> rule3)) -> rule4))] @3: Bob is kind.[(((((((triple3) -> rule5)) -> rule1)) -> rule3))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is not rough.
("Anne" "is" "rough" "-")
triple2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Fiona is cold.
("Fiona" "is" "cold" "+")
triple4
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple5
((triple4) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple6
((triple7 triple5) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((triple7 ((triple4) -> (rule1 % int2))) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple3) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple5) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3