Bob is quiet. Dave is rough. Gary is young. Harry is rough. If something is rough and not young then it is round. All red things are white. If something is young then it is not white. If something is young and not white then it is big. All rough things are not quiet. If something is big then it is quiet.
Bob is quiet.
("Bob" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If something is rough and not young then it is round.
((("something" "is" "rough" "+") ("something" "is" "young" "~")) -> ("something" "is" "round" "+"))
All red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If something is young then it is not white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "-"))
If something is young and not white then it is big.
((("something" "is" "young" "+") ("something" "is" "white" "~")) -> ("something" "is" "big" "+"))
All rough things are not quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "-"))
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Bob is quiet.
True
1
proof
[(triple1)]
("Bob" "is" "quiet" "+")
triple1
Dave is not rough.
False
1
inv-proof
[(triple2)]
("Dave" "is" "rough" "-")
triple2
Harry is not quiet.
True
2
proof
[(((triple4) -> rule5))]
("Harry" "is" "quiet" "-")
((triple4) -> (rule5 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Gary is white.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "white" "+")
((triple3) -> (rule3 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Gary is big.
True
4
proof
[(((triple3 ((triple3) -> rule3)) -> rule4))]
("Gary" "is" "big" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
int2
Gary is not big.
False
4
inv-proof
[(((triple3 ((triple3) -> rule3)) -> rule4))]
("Gary" "is" "big" "-")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
int2
Gary is quiet.
True
5
proof
[(((((triple3 ((triple3) -> rule3)) -> rule4)) -> rule6))]
("Gary" "is" "quiet" "+")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not white.
("Gary" "is" "white" "-")
int3
Gary is not quiet.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule3)) -> rule4)) -> rule6))]
("Gary" "is" "quiet" "-")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not white.
("Gary" "is" "white" "-")
int3
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "round" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "round" "+")
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "white" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "white" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is quiet.[(triple1)] Dave is rough.[(triple2)] Gary is young.[(triple3)] Harry is rough.[(triple4)] @1: Dave is not quiet.[(((triple2) -> rule5))] Gary is not white.[(((triple3) -> rule3))] Harry is not quiet.[(((triple4) -> rule5))] @2: Gary is big.[(((triple3 ((triple3) -> rule3)) -> rule4))] @3: Gary is quiet.[(((((triple3 ((triple3) -> rule3)) -> rule4)) -> rule6))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Dave is not quiet.
("Dave" "is" "quiet" "-")
((triple2) -> (rule5 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Gary is not white.
("Gary" "is" "white" "-")
((triple3) -> (rule3 % int1))
Gary is not white.
("Gary" "is" "white" "-")
int1
Harry is not quiet.
("Harry" "is" "quiet" "-")
((triple4) -> (rule5 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple3 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple3 ((triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not white.
("Gary" "is" "white" "-")
int3