Dave is blue. Dave is green. Dave is kind. Dave is white. Gary is not green. Gary is white. Harry is furry. Harry is green. Harry is smart. Harry is white. All kind people are not big. If Harry is blue and Harry is not green then Harry is not kind. If Gary is green then Gary is furry. If someone is blue and not big then they are furry. If someone is blue and not big then they are white. Furry people are smart.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is white.
("Gary" "is" "white" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
All kind people are not big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "-"))
If Harry is blue and Harry is not green then Harry is not kind.
((("Harry" "is" "blue" "+") ("Harry" "is" "green" "~")) -> ("Harry" "is" "kind" "-"))
If Gary is green then Gary is furry.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "furry" "+"))
If someone is blue and not big then they are furry.
((("someone" "is" "blue" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "furry" "+"))
If someone is blue and not big then they are white.
((("someone" "is" "blue" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "white" "+"))
Furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Dave is kind.
True
1
proof
[(triple3)]
("Dave" "is" "kind" "+")
triple3
Harry is not smart.
False
1
inv-proof
[(triple9 OR ((triple7) -> rule6))]
("Harry" "is" "smart" "-")
triple9
((triple7) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Dave is not big.
True
2
proof
[(((triple3) -> rule1))]
("Dave" "is" "big" "-")
((triple3) -> (rule1 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is big.
False
2
inv-proof
[(((triple3) -> rule1))]
("Dave" "is" "big" "+")
((triple3) -> (rule1 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is furry.
True
4
proof
[(((triple1 ((triple3) -> rule1)) -> rule4))]
("Dave" "is" "furry" "+")
((triple1 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not big.
("Dave" "is" "big" "-")
int2
Dave is not furry.
False
4
inv-proof
[(((triple1 ((triple3) -> rule1)) -> rule4))]
("Dave" "is" "furry" "-")
((triple1 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not big.
("Dave" "is" "big" "-")
int2
Dave is smart.
True
5
proof
[(((((triple1 ((triple3) -> rule1)) -> rule4)) -> rule6))]
("Dave" "is" "smart" "+")
((((triple1 ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not big.
("Dave" "is" "big" "-")
int3
Dave is not smart.
False
5
inv-proof
[(((((triple1 ((triple3) -> rule1)) -> rule4)) -> rule6))]
("Dave" "is" "smart" "-")
((((triple1 ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not big.
("Dave" "is" "big" "-")
int3
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "furry" "-")
Gary is smart.
Unknown
rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Gary" "is" "smart" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Dave is blue.[(triple1)] Dave is green.[(triple2)] Dave is kind.[(triple3)] Dave is white.[(triple4 OR ((triple1 ((triple3) -> rule1)) -> rule5))] Gary is not green.[(triple5)] Gary is white.[(triple6)] Harry is furry.[(triple7)] Harry is green.[(triple8)] Harry is smart.[(triple9 OR ((triple7) -> rule6))] Harry is white.[(triple10)] @1: Dave is not big.[(((triple3) -> rule1))] @2: Dave is furry.[(((triple1 ((triple3) -> rule1)) -> rule4))] @3: Dave is smart.[(((((triple1 ((triple3) -> rule1)) -> rule4)) -> rule6))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
triple4
((triple1 ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is not big.
("Dave" "is" "big" "-")
int2
Gary is not green.
("Gary" "is" "green" "-")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is smart.
("Harry" "is" "smart" "+")
triple9
((triple7) -> (rule6 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple10
Dave is not big.
("Dave" "is" "big" "-")
((triple3) -> (rule1 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((triple1 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not big.
("Dave" "is" "big" "-")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple1 ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not big.
("Dave" "is" "big" "-")
int3