Charlie is smart. Erin is blue. Gary is big. Blue things are nice. Big, nice things are furry. If Charlie is smart and Charlie is blue then Charlie is big. All nice things are big. All white things are nice. Smart things are furry. All cold things are smart. If Charlie is white and Charlie is nice then Charlie is smart.
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is big.
("Gary" "is" "big" "+")
Blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Big, nice things are furry.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If Charlie is smart and Charlie is blue then Charlie is big.
((("Charlie" "is" "smart" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "big" "+"))
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
All white things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
All cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If Charlie is white and Charlie is nice then Charlie is smart.
((("Charlie" "is" "white" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "smart" "+"))
Gary is big.
True
1
proof
[(triple3)]
("Gary" "is" "big" "+")
triple3
Gary is not big.
False
1
inv-proof
[(triple3)]
("Gary" "is" "big" "-")
triple3
Charlie is furry.
True
2
proof
[(((triple1) -> rule6))]
("Charlie" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple1) -> rule6))]
("Charlie" "is" "furry" "-")
((triple1) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Erin is big.
True
3
proof
[(((((triple2) -> rule1)) -> rule4))]
("Erin" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not big.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4))]
("Erin" "is" "big" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is furry.
True
6
proof
[(((((((triple2) -> rule1)) -> rule4) ((triple2) -> rule1)) -> rule2))]
("Erin" "is" "furry" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) ((triple2) -> (rule1 % int3))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is not furry.
False
6
inv-proof
[(((((((triple2) -> rule1)) -> rule4) ((triple2) -> rule1)) -> rule2))]
("Erin" "is" "furry" "-")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) ((triple2) -> (rule1 % int3))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Charlie is not big.
Unknown
inv-rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Charlie" "is" "big" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "nice" "+")
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is smart.[(triple1)] Erin is blue.[(triple2)] Gary is big.[(triple3)] @1: Charlie is furry.[(((triple1) -> rule6))] Erin is nice.[(((triple2) -> rule1))] @2: Erin is big.[(((((triple2) -> rule1)) -> rule4))] @3: Erin is furry.[(((((((triple2) -> rule1)) -> rule4) ((triple2) -> rule1)) -> rule2))]
Charlie is smart.
("Charlie" "is" "smart" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2)) ((triple2) -> (rule1 % int3))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3