Bob is not kind. Fiona is not rough. Gary is not young. Harry is kind. All kind people are quiet. All quiet people are rough. If Harry is rough then Harry is round.
Bob is not kind.
("Bob" "is" "kind" "-")
Fiona is not rough.
("Fiona" "is" "rough" "-")
Gary is not young.
("Gary" "is" "young" "-")
Harry is kind.
("Harry" "is" "kind" "+")
All kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If Harry is rough then Harry is round.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "round" "+"))
Fiona is not rough.
True
1
proof
[(triple2)]
("Fiona" "is" "rough" "-")
triple2
Bob is kind.
False
1
inv-proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Harry is quiet.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "quiet" "+")
((triple4) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple4) -> rule1))]
("Harry" "is" "quiet" "-")
((triple4) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("Harry" "is" "rough" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not rough.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("Harry" "is" "rough" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is round.
True
4
proof
[(((((((triple4) -> rule1)) -> rule2)) -> rule3))]
("Harry" "is" "round" "+")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not round.
False
4
inv-proof
[(((((((triple4) -> rule1)) -> rule2)) -> rule3))]
("Harry" "is" "round" "-")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "quiet" "-")
Bob is rough.
Unknown
rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "rough" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Gary is rough.
Unknown
rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Gary" "is" "rough" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is not kind.[(triple1)] Fiona is not rough.[(triple2)] Gary is not young.[(triple3)] Harry is kind.[(triple4)] @1: Harry is quiet.[(((triple4) -> rule1))] @2: Harry is rough.[(((((triple4) -> rule1)) -> rule2))] @3: Harry is round.[(((((((triple4) -> rule1)) -> rule2)) -> rule3))]
Bob is not kind.
("Bob" "is" "kind" "-")
triple1
Fiona is not rough.
("Fiona" "is" "rough" "-")
triple2
Gary is not young.
("Gary" "is" "young" "-")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((((triple4) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3