Erin is big. Erin is red. Gary is furry. All smart people are nice. Quiet people are cold. All big people are cold. Quiet people are furry. Big people are smart. All furry people are big.
Erin is big.
("Erin" "is" "big" "+")
Erin is red.
("Erin" "is" "red" "+")
Gary is furry.
("Gary" "is" "furry" "+")
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Quiet people are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
All big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
Quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
Big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
All furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
Erin is red.
True
1
proof
[(triple2)]
("Erin" "is" "red" "+")
triple2
Gary is not furry.
False
1
inv-proof
[(triple3)]
("Gary" "is" "furry" "-")
triple3
Erin is cold.
True
2
proof
[(((triple1) -> rule3))]
("Erin" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple1) -> rule5))]
("Erin" "is" "smart" "-")
((triple1) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is cold.
True
3
proof
[(((((triple3) -> rule6)) -> rule3))]
("Gary" "is" "cold" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule5))]
("Gary" "is" "smart" "-")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
True
4
proof
[(((((((triple3) -> rule6)) -> rule5)) -> rule1))]
("Gary" "is" "nice" "+")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is not nice.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule5)) -> rule1))]
("Gary" "is" "nice" "-")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "furry" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Erin is big.[(triple1)] Erin is red.[(triple2)] Gary is furry.[(triple3)] @1: Erin is cold.[(((triple1) -> rule3))] Erin is smart.[(((triple1) -> rule5))] Gary is big.[(((triple3) -> rule6))] @2: Erin is nice.[(((((triple1) -> rule5)) -> rule1))] Gary is cold.[(((((triple3) -> rule6)) -> rule3))] Gary is smart.[(((((triple3) -> rule6)) -> rule5))] @3: Gary is nice.[(((((((triple3) -> rule6)) -> rule5)) -> rule1))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple1) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple3) -> (rule6 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3