Charlie is big. Erin is big. Erin is red. If Erin is not smart then Erin is not white. Smart people are red. Smart people are red. Furry people are red. All furry people are cold. If Erin is blue and Erin is cold then Erin is furry. All big people are furry. Red, furry people are white.
Charlie is big.
("Charlie" "is" "big" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is red.
("Erin" "is" "red" "+")
If Erin is not smart then Erin is not white.
((("Erin" "is" "smart" "~")) -> ("Erin" "is" "white" "-"))
Smart people are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Smart people are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
All furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If Erin is blue and Erin is cold then Erin is furry.
((("Erin" "is" "blue" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "furry" "+"))
All big people are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Red, furry people are white.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Erin is not red.
False
1
inv-proof
[(triple3 OR ((((triple2) -> rule7)) -> rule4))]
("Erin" "is" "red" "-")
triple3
((((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is furry.
True
2
proof
[(((triple2) -> rule7))]
("Erin" "is" "furry" "+")
((triple2) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not furry.
False
2
inv-proof
[(((triple2) -> rule7))]
("Erin" "is" "furry" "-")
((triple2) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Charlie is red.
True
3
proof
[(((((triple1) -> rule7)) -> rule4))]
("Charlie" "is" "red" "+")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Erin is not cold.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule5))]
("Erin" "is" "cold" "-")
((((triple2) -> (rule7 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Charlie is white.
True
6
proof
[(((((((triple1) -> rule7)) -> rule4) ((triple1) -> rule7)) -> rule8))]
("Charlie" "is" "white" "+")
((((((triple1) -> (rule7 % int3))) -> (rule4 % int2)) ((triple1) -> (rule7 % int3))) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not white.
False
6
inv-proof
[(((((((triple1) -> rule7)) -> rule4) ((triple1) -> rule7)) -> rule8))]
("Charlie" "is" "white" "-")
((((((triple1) -> (rule7 % int3))) -> (rule4 % int2)) ((triple1) -> (rule7 % int3))) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is big.[(triple1)] Erin is big.[(triple2)] Erin is red.[(triple3 OR ((((triple2) -> rule7)) -> rule4))] @1: Charlie is furry.[(((triple1) -> rule7))] Erin is furry.[(((triple2) -> rule7))] @2: Charlie is cold.[(((((triple1) -> rule7)) -> rule5))] Charlie is red.[(((((triple1) -> rule7)) -> rule4))] Erin is cold.[(((((triple2) -> rule7)) -> rule5))] Erin is white.[(((triple3 ((triple2) -> rule7)) -> rule8) OR ((((((triple2) -> rule7)) -> rule4) ((triple2) -> rule7)) -> rule8))] @3: Charlie is white.[(((((((triple1) -> rule7)) -> rule4) ((triple1) -> rule7)) -> rule8))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
((((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple2) -> (rule7 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((triple2) -> (rule7 % int2))) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((triple3 ((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((((triple2) -> (rule7 % int3))) -> (rule4 % int2)) ((triple2) -> (rule7 % int3))) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
((((((triple1) -> (rule7 % int3))) -> (rule4 % int2)) ((triple1) -> (rule7 % int3))) -> (rule8 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3