Charlie is green. Charlie is white. Dave is red. Big things are white. If something is green and white then it is big. Furry, big things are red. All kind, red things are big. If Dave is red and Dave is green then Dave is furry. Red things are kind. All red things are smart. If Charlie is red then Charlie is kind.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is red.
("Dave" "is" "red" "+")
Big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is green and white then it is big.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
Furry, big things are red.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
All kind, red things are big.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If Dave is red and Dave is green then Dave is furry.
((("Dave" "is" "red" "+") ("Dave" "is" "green" "+")) -> ("Dave" "is" "furry" "+"))
Red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
All red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If Charlie is red then Charlie is kind.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "kind" "+"))
Dave is red.
True
1
proof
[(triple3)]
("Dave" "is" "red" "+")
triple3
Dave is not red.
False
1
inv-proof
[(triple3)]
("Dave" "is" "red" "-")
triple3
Dave is smart.
True
2
proof
[(((triple3) -> rule7))]
("Dave" "is" "smart" "+")
((triple3) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple3) -> rule7))]
("Dave" "is" "smart" "-")
((triple3) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
True
4
proof
[(((((triple3) -> rule6) triple3) -> rule4))]
("Dave" "is" "big" "+")
((((triple3) -> (rule6 % int2)) triple3) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not big.
False
4
inv-proof
[(((((triple3) -> rule6) triple3) -> rule4))]
("Dave" "is" "big" "-")
((((triple3) -> (rule6 % int2)) triple3) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is white.
True
5
proof
[(((((((triple3) -> rule6) triple3) -> rule4)) -> rule1))]
("Dave" "is" "white" "+")
((((((triple3) -> (rule6 % int3)) triple3) -> (rule4 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not white.
False
5
inv-proof
[(((((((triple3) -> rule6) triple3) -> rule4)) -> rule1))]
("Dave" "is" "white" "-")
((((((triple3) -> (rule6 % int3)) triple3) -> (rule4 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "furry" "-")
Charlie is red.
Unknown
rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "red" "+")
Charlie is not smart.
Unknown
inv-rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule7 <- rule3 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is kind.
Unknown
rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Charlie is green.[(triple1)] Charlie is white.[(triple2)] Dave is red.[(triple3)] @1: Charlie is big.[(((triple1 triple2) -> rule2))] Dave is kind.[(((triple3) -> rule6))] Dave is smart.[(((triple3) -> rule7))] @2: Dave is big.[(((((triple3) -> rule6) triple3) -> rule4))] @3: Dave is white.[(((((((triple3) -> rule6) triple3) -> rule4)) -> rule1))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
((triple1 triple2) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple3) -> (rule6 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple3) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple3) -> (rule6 % int2)) triple3) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((((((triple3) -> (rule6 % int3)) triple3) -> (rule4 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3