Dave is white. Erin is furry. Gary is not blue. Harry is young. If someone is red then they are big. If Gary is red then Gary is young. All big, young people are blue. If someone is white and furry then they are not blue. If someone is blue and furry then they are cold. Big people are not cold. All furry people are red. If someone is cold and not white then they are furry.
Dave is white.
("Dave" "is" "white" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Harry is young.
("Harry" "is" "young" "+")
If someone is red then they are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If Gary is red then Gary is young.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "young" "+"))
All big, young people are blue.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
If someone is white and furry then they are not blue.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "-"))
If someone is blue and furry then they are cold.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Big people are not cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "-"))
All furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If someone is cold and not white then they are furry.
((("someone" "is" "cold" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "furry" "+"))
Erin is furry.
True
1
proof
[(triple2)]
("Erin" "is" "furry" "+")
triple2
Erin is not furry.
False
1
inv-proof
[(triple2)]
("Erin" "is" "furry" "-")
triple2
Erin is red.
True
2
proof
[(((triple2) -> rule7))]
("Erin" "is" "red" "+")
((triple2) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple2) -> rule7))]
("Erin" "is" "red" "-")
((triple2) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
True
3
proof
[(((((triple2) -> rule7)) -> rule1))]
("Erin" "is" "big" "+")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not big.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule1))]
("Erin" "is" "big" "-")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not cold.
True
4
proof
[(((((((triple2) -> rule7)) -> rule1)) -> rule6))]
("Erin" "is" "cold" "-")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is cold.
False
4
inv-proof
[(((((((triple2) -> rule7)) -> rule1)) -> rule6))]
("Erin" "is" "cold" "+")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "blue" "-")
Gary is red.
Unknown
rconc
[@2: Gary is red.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("Gary" "is" "red" "+")
Harry is not big.
Unknown
inv-rconc
[@3: Harry is big.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule8 <- FAIL)]]
("Harry" "is" "big" "-")
Harry is cold.
Unknown
rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("Harry" "is" "cold" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Dave is white.[(triple1)] Erin is furry.[(triple2)] Gary is not blue.[(triple3)] Harry is young.[(triple4)] @1: Erin is red.[(((triple2) -> rule7))] @2: Erin is big.[(((((triple2) -> rule7)) -> rule1))] @3: Erin is not cold.[(((((((triple2) -> rule7)) -> rule1)) -> rule6))]
Dave is white.
("Dave" "is" "white" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Gary is not blue.
("Gary" "is" "blue" "-")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
((triple2) -> (rule7 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is not cold.
("Erin" "is" "cold" "-")
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Erin is not cold.
("Erin" "is" "cold" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3