Bob is not quiet. Dave is smart. Gary is big. Harry is rough. All quiet people are nice. Quiet, rough people are nice. If Dave is not rough then Dave is smart. White, rough people are smart. If someone is rough then they are white. All smart people are quiet. If Bob is big and Bob is not quiet then Bob is not nice. All smart, nice people are not round.
Bob is not quiet.
("Bob" "is" "quiet" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is big.
("Gary" "is" "big" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Quiet, rough people are nice.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If Dave is not rough then Dave is smart.
((("Dave" "is" "rough" "~")) -> ("Dave" "is" "smart" "+"))
White, rough people are smart.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is rough then they are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
All smart people are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If Bob is big and Bob is not quiet then Bob is not nice.
((("Bob" "is" "big" "+") ("Bob" "is" "quiet" "~")) -> ("Bob" "is" "nice" "-"))
All smart, nice people are not round.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "-"))
Harry is rough.
True
1
proof
[(triple4)]
("Harry" "is" "rough" "+")
triple4
Dave is not smart.
False
1
inv-proof
[(triple2)]
("Dave" "is" "smart" "-")
triple2
Harry is white.
True
2
proof
[(((triple4) -> rule5))]
("Harry" "is" "white" "+")
((triple4) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple2) -> rule6))]
("Dave" "is" "quiet" "-")
((triple2) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is smart.
True
4
proof
[(((((triple4) -> rule5) triple4) -> rule4))]
("Harry" "is" "smart" "+")
((((triple4) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not smart.
False
4
inv-proof
[(((((triple4) -> rule5) triple4) -> rule4))]
("Harry" "is" "smart" "-")
((((triple4) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "smart" "+")
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "white" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is not quiet.[(triple1)] Dave is smart.[(triple2)] Gary is big.[(triple3)] Harry is rough.[(triple4)] @1: Dave is quiet.[(((triple2) -> rule6))] Harry is white.[(((triple4) -> rule5))] @2: Dave is nice.[(((((triple2) -> rule6)) -> rule1))] Harry is smart.[(((((triple4) -> rule5) triple4) -> rule4))] @3: Dave is not round.[(((triple2 ((((triple2) -> rule6)) -> rule1)) -> rule8))] Harry is quiet.[(((((((triple4) -> rule5) triple4) -> rule4)) -> rule6))] @4: Harry is nice.[(((((((((triple4) -> rule5) triple4) -> rule4)) -> rule6)) -> rule1) OR ((((((((triple4) -> rule5) triple4) -> rule4)) -> rule6) triple4) -> rule2))] @5: Harry is not round.[(((((((triple4) -> rule5) triple4) -> rule4) ((((((((triple4) -> rule5) triple4) -> rule4)) -> rule6)) -> rule1)) -> rule8) OR ((((((triple4) -> rule5) triple4) -> rule4) ((((((((triple4) -> rule5) triple4) -> rule4)) -> rule6) triple4) -> rule2)) -> rule8))]
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((((triple4) -> (rule5 % int2)) triple4) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Dave is not round.
("Dave" "is" "round" "-")
((triple2 ((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
((((((triple4) -> (rule5 % int3)) triple4) -> (rule4 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
((((((((triple4) -> (rule5 % int4)) triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
((((((((triple4) -> (rule5 % int4)) triple4) -> (rule4 % int3))) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
int4
Harry is not round.
("Harry" "is" "round" "-")
((((((triple4) -> (rule5 % int5)) triple4) -> (rule4 % int4)) ((((((((triple4) -> (rule5 % int5)) triple4) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
int5
((((((triple4) -> (rule5 % int5)) triple4) -> (rule4 % int4)) ((((((((triple4) -> (rule5 % int5)) triple4) -> (rule4 % int4))) -> (rule6 % int3)) triple4) -> (rule2 % int2))) -> (rule8 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is white.
("Harry" "is" "white" "+")
int5