Charlie is cold. Dave is big. Dave is red. Gary is cold. Gary is quiet. Gary is red. Harry is big. Harry is cold. Harry is furry. Harry is red. Harry is rough. Harry is white. All white people are rough. Furry people are rough. If Harry is big then Harry is red. All red, big people are rough. Cold people are big. All furry, quiet people are rough. If Dave is red then Dave is furry. All cold, white people are furry.
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is red.
("Dave" "is" "red" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
All white people are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
Furry people are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If Harry is big then Harry is red.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "red" "+"))
All red, big people are rough.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
All furry, quiet people are rough.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If Dave is red then Dave is furry.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "furry" "+"))
All cold, white people are furry.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Dave is big.
True
1
proof
[(triple2)]
("Dave" "is" "big" "+")
triple2
Gary is not cold.
False
1
inv-proof
[(triple4)]
("Gary" "is" "cold" "-")
triple4
Charlie is big.
True
2
proof
[(((triple1) -> rule5))]
("Charlie" "is" "big" "+")
((triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple1) -> rule5))]
("Charlie" "is" "big" "-")
((triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "furry" "-")
Charlie is rough.
Unknown
rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- rule8 <- FAIL)]]
("Charlie" "is" "rough" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Charlie is cold.[(triple1)] Dave is big.[(triple2)] Dave is red.[(triple3)] Gary is cold.[(triple4)] Gary is quiet.[(triple5)] Gary is red.[(triple6)] Harry is big.[(triple7 OR ((triple8) -> rule5))] Harry is cold.[(triple8)] Harry is furry.[(triple9 OR ((triple8 triple12) -> rule8))] Harry is red.[(triple10 OR ((triple7) -> rule3) OR ((((triple8) -> rule5)) -> rule3))] Harry is rough.[(triple11 OR ((triple12) -> rule1) OR ((triple9) -> rule2) OR ((triple10 triple7) -> rule4) OR ((((triple8 triple12) -> rule8)) -> rule2) OR ((triple10 ((triple8) -> rule5)) -> rule4) OR ((((triple7) -> rule3) triple7) -> rule4) OR ((((triple7) -> rule3) ((triple8) -> rule5)) -> rule4) OR ((((((triple8) -> rule5)) -> rule3) triple7) -> rule4) OR ((((((triple8) -> rule5)) -> rule3) ((triple8) -> rule5)) -> rule4))] Harry is white.[(triple12)] @1: Charlie is big.[(((triple1) -> rule5))] Dave is furry.[(((triple3) -> rule7))] Dave is rough.[(((triple3 triple2) -> rule4) OR ((((triple3) -> rule7)) -> rule2))] Gary is big.[(((triple4) -> rule5))] @2: Gary is rough.[(((triple6 ((triple4) -> rule5)) -> rule4))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
((triple8) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is furry.
("Harry" "is" "furry" "+")
triple9
((triple8 triple12) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple10
((triple7) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple11
((triple12) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple9) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple10 triple7) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple8 triple12) -> (rule8 % int2))) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((triple10 ((triple8) -> (rule5 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((triple7) -> (rule3 % int2)) triple7) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple7) -> (rule3 % int3)) ((triple8) -> (rule5 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((((triple8) -> (rule5 % int3))) -> (rule3 % int2)) triple7) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
((((((triple8) -> (rule5 % int3))) -> (rule3 % int2)) ((triple8) -> (rule5 % int3))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
triple12
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple3) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple3 triple2) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((triple4) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple6 ((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2