Dave is big. Dave is cold. Dave is quiet. Dave is rough. Dave is smart. Dave is white. Gary is big. Gary is cold. Gary is rough. Gary is smart. Harry is cold. Harry is nice. Harry is quiet. Harry is rough. Harry is smart. Harry is white. All smart, rough people are big. If Harry is white then Harry is quiet. All smart people are rough. White, rough people are big. White, rough people are nice. If Gary is quiet and Gary is big then Gary is white.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
All smart, rough people are big.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If Harry is white then Harry is quiet.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "quiet" "+"))
All smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
White, rough people are big.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
White, rough people are nice.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If Gary is quiet and Gary is big then Gary is white.
((("Gary" "is" "quiet" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "white" "+"))
Gary is big.
True
1
proof
[(triple7 OR ((triple10 triple9) -> rule1) OR ((triple10 ((triple10) -> rule3)) -> rule1))]
("Gary" "is" "big" "+")
triple7
((triple10 triple9) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple10 ((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not smart.
False
1
inv-proof
[(triple10)]
("Gary" "is" "smart" "-")
triple10
Dave is nice.
True
3
proof
[(((triple6 triple4) -> rule5) OR ((triple6 ((triple5) -> rule3)) -> rule5))]
("Dave" "is" "nice" "+")
((triple6 triple4) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple6 ((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Harry is not big.
False
3
inv-proof
[(((triple15 triple14) -> rule1) OR ((triple16 triple14) -> rule4) OR ((triple15 ((triple15) -> rule3)) -> rule1) OR ((triple16 ((triple15) -> rule3)) -> rule4))]
("Harry" "is" "big" "-")
((triple15 triple14) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple16 triple14) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple15 ((triple15) -> (rule3 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple16 ((triple15) -> (rule3 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is nice.
Unknown
rconc
[@2: Gary is nice.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Gary" "is" "nice" "+")
@0: Dave is big.[(triple1 OR ((triple5 triple4) -> rule1) OR ((triple6 triple4) -> rule4) OR ((triple5 ((triple5) -> rule3)) -> rule1) OR ((triple6 ((triple5) -> rule3)) -> rule4))] Dave is cold.[(triple2)] Dave is quiet.[(triple3)] Dave is rough.[(triple4 OR ((triple5) -> rule3))] Dave is smart.[(triple5)] Dave is white.[(triple6)] Gary is big.[(triple7 OR ((triple10 triple9) -> rule1) OR ((triple10 ((triple10) -> rule3)) -> rule1))] Gary is cold.[(triple8)] Gary is rough.[(triple9 OR ((triple10) -> rule3))] Gary is smart.[(triple10)] Harry is cold.[(triple11)] Harry is nice.[(triple12 OR ((triple16 triple14) -> rule5) OR ((triple16 ((triple15) -> rule3)) -> rule5))] Harry is quiet.[(triple13 OR ((triple16) -> rule2))] Harry is rough.[(triple14 OR ((triple15) -> rule3))] Harry is smart.[(triple15)] Harry is white.[(triple16)] @1: Dave is nice.[(((triple6 triple4) -> rule5) OR ((triple6 ((triple5) -> rule3)) -> rule5))] Harry is big.[(((triple15 triple14) -> rule1) OR ((triple16 triple14) -> rule4) OR ((triple15 ((triple15) -> rule3)) -> rule1) OR ((triple16 ((triple15) -> rule3)) -> rule4))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((triple5 triple4) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple6 triple4) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple5 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
((triple6 ((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
((triple5) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
((triple10 triple9) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple10 ((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is rough.
("Gary" "is" "rough" "+")
triple9
((triple10) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Harry is cold.
("Harry" "is" "cold" "+")
triple11
Harry is nice.
("Harry" "is" "nice" "+")
triple12
((triple16 triple14) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((triple16 ((triple15) -> (rule3 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
((triple16) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple14
((triple15) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
triple16
Dave is nice.
("Dave" "is" "nice" "+")
((triple6 triple4) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple6 ((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((triple15 triple14) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple16 triple14) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple15 ((triple15) -> (rule3 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((triple16 ((triple15) -> (rule3 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2