Charlie is big. Charlie is smart. Dave is big. If Charlie is nice and Charlie is not big then Charlie is smart. White, big people are furry. If someone is big and round then they are white. If Dave is smart then Dave is green. Smart people are round. If someone is white then they are not nice.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
If Charlie is nice and Charlie is not big then Charlie is smart.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "big" "~")) -> ("Charlie" "is" "smart" "+"))
White, big people are furry.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
If someone is big and round then they are white.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If Dave is smart then Dave is green.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "green" "+"))
Smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If someone is white then they are not nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "-"))
Dave is big.
True
1
proof
[(triple3)]
("Dave" "is" "big" "+")
triple3
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Charlie is round.
True
2
proof
[(((triple2) -> rule5))]
("Charlie" "is" "round" "+")
((triple2) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not round.
False
2
inv-proof
[(((triple2) -> rule5))]
("Charlie" "is" "round" "-")
((triple2) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
True
4
proof
[(((triple1 ((triple2) -> rule5)) -> rule3))]
("Charlie" "is" "white" "+")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not white.
False
4
inv-proof
[(((triple1 ((triple2) -> rule5)) -> rule3))]
("Charlie" "is" "white" "-")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not furry.
Unknown
inv-rconc
[@3: Dave is furry.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule5 <- FAIL)]]
("Dave" "is" "furry" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Charlie is big.[(triple1)] Charlie is smart.[(triple2)] Dave is big.[(triple3)] @1: Charlie is round.[(((triple2) -> rule5))] @2: Charlie is white.[(((triple1 ((triple2) -> rule5)) -> rule3))] @3: Charlie is furry.[(((((triple1 ((triple2) -> rule5)) -> rule3) triple1) -> rule2))] Charlie is not nice.[(((((triple1 ((triple2) -> rule5)) -> rule3)) -> rule6))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
((triple2) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple1 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple1 ((triple2) -> (rule5 % int3))) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is not nice.
("Charlie" "is" "nice" "-")
((((triple1 ((triple2) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3