Bob is kind. Bob is nice. Bob is rough. Bob is white. Gary is blue. Gary is quiet. Gary is white. If someone is white then they are nice. If someone is white and not quiet then they are nice. If someone is nice then they are rough. If Bob is nice and Bob is rough then Bob is white. All quiet people are white. If someone is quiet and not rough then they are round. Blue, white people are not round. If someone is rough and not round then they are kind.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is white then they are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If someone is white and not quiet then they are nice.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If Bob is nice and Bob is rough then Bob is white.
((("Bob" "is" "nice" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "white" "+"))
All quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is quiet and not rough then they are round.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "round" "+"))
Blue, white people are not round.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "-"))
If someone is rough and not round then they are kind.
((("someone" "is" "rough" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "kind" "+"))
Gary is quiet.
True
1
proof
[(triple6)]
("Gary" "is" "quiet" "+")
triple6
Bob is not rough.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule3) OR ((((triple4) -> rule1)) -> rule3))]
("Bob" "is" "rough" "-")
triple3
((triple2) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Gary is not round.
True
3
proof
[(((triple5 triple7) -> rule7) OR ((triple5 ((triple6) -> rule5)) -> rule7))]
("Gary" "is" "round" "-")
((triple5 triple7) -> (rule7 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
((triple5 ((triple6) -> (rule5 % int2))) -> (rule7 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is round.
False
3
inv-proof
[(((triple5 triple7) -> rule7) OR ((triple5 ((triple6) -> rule5)) -> rule7))]
("Gary" "is" "round" "+")
((triple5 triple7) -> (rule7 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
((triple5 ((triple6) -> (rule5 % int2))) -> (rule7 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
True
3
proof
[(((((triple7) -> rule1)) -> rule3) OR ((((((triple6) -> rule5)) -> rule1)) -> rule3))]
("Gary" "is" "rough" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not rough.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule3) OR ((((((triple6) -> rule5)) -> rule1)) -> rule3))]
("Gary" "is" "rough" "-")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is kind.[(triple1)] Bob is nice.[(triple2 OR ((triple4) -> rule1))] Bob is rough.[(triple3 OR ((triple2) -> rule3) OR ((((triple4) -> rule1)) -> rule3))] Bob is white.[(triple4 OR ((triple2 triple3) -> rule4) OR ((triple2 ((triple2) -> rule3)) -> rule4))] Gary is blue.[(triple5)] Gary is quiet.[(triple6)] Gary is white.[(triple7 OR ((triple6) -> rule5))] @1: Gary is nice.[(((triple7) -> rule1) OR ((((triple6) -> rule5)) -> rule1))] Gary is not round.[(((triple5 triple7) -> rule7) OR ((triple5 ((triple6) -> rule5)) -> rule7))] @2: Gary is rough.[(((((triple7) -> rule1)) -> rule3) OR ((((((triple6) -> rule5)) -> rule1)) -> rule3))] @3: Gary is kind.[(((((((triple7) -> rule1)) -> rule3) ((triple5 triple7) -> rule7)) -> rule8) OR ((((((triple7) -> rule1)) -> rule3) ((triple5 ((triple6) -> rule5)) -> rule7)) -> rule8) OR ((((((((triple6) -> rule5)) -> rule1)) -> rule3) ((triple5 triple7) -> rule7)) -> rule8) OR ((((((((triple6) -> rule5)) -> rule1)) -> rule3) ((triple5 ((triple6) -> rule5)) -> rule7)) -> rule8))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
((triple4) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple3
((triple2) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple4
((triple2 triple3) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
((triple6) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple7) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple6) -> (rule5 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not round.
("Gary" "is" "round" "-")
((triple5 triple7) -> (rule7 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
((triple5 ((triple6) -> (rule5 % int2))) -> (rule7 % int1))
Gary is not round.
("Gary" "is" "round" "-")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((((triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
((((((triple7) -> (rule1 % int4))) -> (rule3 % int3)) ((triple5 triple7) -> (rule7 % int2))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not round.
("Gary" "is" "round" "-")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
((((((triple7) -> (rule1 % int5))) -> (rule3 % int4)) ((triple5 ((triple6) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not round.
("Gary" "is" "round" "-")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is nice.
("Gary" "is" "nice" "+")
int5
((((((((triple6) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule3 % int3)) ((triple5 triple7) -> (rule7 % int2))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not round.
("Gary" "is" "round" "-")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
int5
((((((((triple6) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule3 % int3)) ((triple5 ((triple6) -> (rule5 % int5))) -> (rule7 % int2))) -> (rule8 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not round.
("Gary" "is" "round" "-")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
int5