Charlie is blue. Charlie is kind. Charlie is quiet. Dave is smart. Gary is furry. Gary is quiet. Gary is smart. If someone is white then they are big. If someone is quiet then they are white. If someone is quiet and white then they are kind. If Dave is quiet then Dave is big. If Charlie is blue then Charlie is smart. If Gary is smart and Gary is furry then Gary is big.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If someone is white then they are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is quiet and white then they are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If Dave is quiet then Dave is big.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "big" "+"))
If Charlie is blue then Charlie is smart.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "smart" "+"))
If Gary is smart and Gary is furry then Gary is big.
((("Gary" "is" "smart" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "big" "+"))
Charlie is kind.
True
1
proof
[(triple2 OR ((triple3 ((triple3) -> rule2)) -> rule3))]
("Charlie" "is" "kind" "+")
triple2
((triple3 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Gary is not smart.
False
1
inv-proof
[(triple7)]
("Gary" "is" "smart" "-")
triple7
Gary is big.
True
3
proof
[(((triple7 triple5) -> rule6) OR ((((triple6) -> rule2)) -> rule1))]
("Gary" "is" "big" "+")
((triple7 triple5) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not white.
False
2
inv-proof
[(((triple6) -> rule2))]
("Gary" "is" "white" "-")
((triple6) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is not big.
Unknown
inv-rconc
[@2: Dave is big.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "big" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "kind" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Charlie is blue.[(triple1)] Charlie is kind.[(triple2 OR ((triple3 ((triple3) -> rule2)) -> rule3))] Charlie is quiet.[(triple3)] Dave is smart.[(triple4)] Gary is furry.[(triple5)] Gary is quiet.[(triple6)] Gary is smart.[(triple7)] @1: Charlie is smart.[(((triple1) -> rule5))] Charlie is white.[(((triple3) -> rule2))] Gary is big.[(((triple7 triple5) -> rule6) OR ((((triple6) -> rule2)) -> rule1))] Gary is white.[(((triple6) -> rule2))] @2: Charlie is big.[(((((triple3) -> rule2)) -> rule1))] Gary is kind.[(((triple6 ((triple6) -> rule2)) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
((triple3 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple3) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple7 triple5) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple6) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((triple6 ((triple6) -> (rule2 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2