Bob is furry. Charlie is not quiet. Fiona is green. All kind, young people are rough. If someone is quiet and green then they are rough. All round people are rough. All rough, kind people are quiet. If someone is furry then they are quiet. Furry, round people are young. Young, round people are furry. If someone is quiet then they are round.
Bob is furry.
("Bob" "is" "furry" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Fiona is green.
("Fiona" "is" "green" "+")
All kind, young people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is quiet and green then they are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
All round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All rough, kind people are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If someone is furry then they are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Furry, round people are young.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Young, round people are furry.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
If someone is quiet then they are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Charlie is not quiet.
True
1
proof
[(triple2)]
("Charlie" "is" "quiet" "-")
triple2
Bob is not furry.
False
1
inv-proof
[(triple1)]
("Bob" "is" "furry" "-")
triple1
Bob is quiet.
True
2
proof
[(((triple1) -> rule5))]
("Bob" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple1) -> rule5))]
("Bob" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
True
3
proof
[(((((triple1) -> rule5)) -> rule8))]
("Bob" "is" "round" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not round.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule8))]
("Bob" "is" "round" "-")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is rough.
True
4
proof
[(((((((triple1) -> rule5)) -> rule8)) -> rule3))]
("Bob" "is" "rough" "+")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not rough.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule8)) -> rule3))]
("Bob" "is" "rough" "-")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Fiona is not young.
Unknown
inv-rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Fiona" "is" "young" "-")
Charlie is furry.
Unknown
rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not round.
Unknown
inv-rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "round" "-")
Fiona is quiet.
Unknown
rconc
[@3: Fiona is quiet.[CWA. Example of deepest failure = (rule5 <- rule7 <- rule6 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is furry.[(triple1)] Charlie is not quiet.[(triple2)] Fiona is green.[(triple3)] @1: Bob is quiet.[(((triple1) -> rule5))] @2: Bob is round.[(((((triple1) -> rule5)) -> rule8))] @3: Bob is rough.[(((((((triple1) -> rule5)) -> rule8)) -> rule3))] Bob is young.[(((triple1 ((((triple1) -> rule5)) -> rule8)) -> rule6))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple2
Fiona is green.
("Fiona" "is" "green" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is young.
("Bob" "is" "young" "+")
((triple1 ((((triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3