Dave is not rough. Erin is quiet. Fiona is kind. If someone is round then they are smart. Round people are smart. If someone is kind then they are round. All round people are rough. If someone is kind and not young then they are rough. If someone is kind and rough then they are not quiet. If Dave is young then Dave is not quiet. If Fiona is not round then Fiona is not quiet.
Dave is not rough.
("Dave" "is" "rough" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
If someone is round then they are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
If someone is kind then they are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
All round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind and not young then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "rough" "+"))
If someone is kind and rough then they are not quiet.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "-"))
If Dave is young then Dave is not quiet.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "quiet" "-"))
If Fiona is not round then Fiona is not quiet.
((("Fiona" "is" "round" "~")) -> ("Fiona" "is" "quiet" "-"))
Fiona is kind.
True
1
proof
[(triple3)]
("Fiona" "is" "kind" "+")
triple3
Fiona is not kind.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "kind" "-")
triple3
Fiona is round.
True
2
proof
[(((triple3) -> rule3))]
("Fiona" "is" "round" "+")
((triple3) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is not round.
False
2
inv-proof
[(((triple3) -> rule3))]
("Fiona" "is" "round" "-")
((triple3) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is rough.
True
3
proof
[(((((triple3) -> rule3)) -> rule4))]
("Fiona" "is" "rough" "+")
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is not rough.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule4))]
("Fiona" "is" "rough" "-")
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is not quiet.
True
5
proof
[(((triple3 ((((triple3) -> rule3)) -> rule4)) -> rule6))]
("Fiona" "is" "quiet" "-")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Fiona is quiet.
False
5
inv-proof
[(((triple3 ((((triple3) -> rule3)) -> rule4)) -> rule6))]
("Fiona" "is" "quiet" "+")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Erin is smart.
Unknown
rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Erin" "is" "smart" "+")
Dave is not smart.
Unknown
inv-rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Dave" "is" "smart" "-")
Erin is round.
Unknown
rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "round" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Dave is not rough.[(triple1)] Erin is quiet.[(triple2)] Fiona is kind.[(triple3)] @1: Fiona is round.[(((triple3) -> rule3))] @2: Fiona is rough.[(((((triple3) -> rule3)) -> rule4))] Fiona is smart.[(((((triple3) -> rule3)) -> rule1) OR ((((triple3) -> rule3)) -> rule2))] @3: Fiona is not quiet.[(((triple3 ((((triple3) -> rule3)) -> rule4)) -> rule6))]
Dave is not rough.
("Dave" "is" "rough" "-")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple3
Fiona is round.
("Fiona" "is" "round" "+")
((triple3) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
((triple3 ((((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
int3