Erin is cold. Erin is round. Erin is white. Harry is big. Harry is cold. Harry is kind. Harry is quiet. All kind people are big. If Erin is kind then Erin is cold. Blue, white people are round. White, kind people are blue. Kind people are white. If Harry is quiet then Harry is blue. Kind people are blue. If someone is kind then they are cold.
Erin is cold.
("Erin" "is" "cold" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
All kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If Erin is kind then Erin is cold.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "cold" "+"))
Blue, white people are round.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
White, kind people are blue.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Kind people are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
If Harry is quiet then Harry is blue.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "blue" "+"))
Kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is kind then they are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Erin is round.
True
1
proof
[(triple2)]
("Erin" "is" "round" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple5 OR ((triple6) -> rule8))]
("Harry" "is" "cold" "-")
triple5
((triple6) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
True
2
proof
[(((triple6) -> rule5))]
("Harry" "is" "white" "+")
((triple6) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not blue.
False
2
inv-proof
[(((triple6) -> rule7) OR ((triple7) -> rule6) OR ((((triple6) -> rule5) triple6) -> rule4))]
("Harry" "is" "blue" "-")
((triple6) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple7) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple6) -> (rule5 % int2)) triple6) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is round.
True
5
proof
[(((((triple6) -> rule7) ((triple6) -> rule5)) -> rule3) OR ((((triple7) -> rule6) ((triple6) -> rule5)) -> rule3) OR ((((((triple6) -> rule5) triple6) -> rule4) ((triple6) -> rule5)) -> rule3))]
("Harry" "is" "round" "+")
((((triple6) -> (rule7 % int3)) ((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((triple7) -> (rule6 % int3)) ((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple6) -> (rule5 % int3)) triple6) -> (rule4 % int2)) ((triple6) -> (rule5 % int3))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is not round.
False
5
inv-proof
[(((((triple6) -> rule7) ((triple6) -> rule5)) -> rule3) OR ((((triple7) -> rule6) ((triple6) -> rule5)) -> rule3) OR ((((((triple6) -> rule5) triple6) -> rule4) ((triple6) -> rule5)) -> rule3))]
("Harry" "is" "round" "-")
((((triple6) -> (rule7 % int3)) ((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((triple7) -> (rule6 % int3)) ((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple6) -> (rule5 % int3)) triple6) -> (rule4 % int2)) ((triple6) -> (rule5 % int3))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "blue" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "big" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Erin is cold.[(triple1)] Erin is round.[(triple2)] Erin is white.[(triple3)] Harry is big.[(triple4 OR ((triple6) -> rule1))] Harry is cold.[(triple5 OR ((triple6) -> rule8))] Harry is kind.[(triple6)] Harry is quiet.[(triple7)] @1: Harry is blue.[(((triple6) -> rule7) OR ((triple7) -> rule6) OR ((((triple6) -> rule5) triple6) -> rule4))] Harry is white.[(((triple6) -> rule5))] @2: Harry is round.[(((((triple6) -> rule7) ((triple6) -> rule5)) -> rule3) OR ((((triple7) -> rule6) ((triple6) -> rule5)) -> rule3) OR ((((((triple6) -> rule5) triple6) -> rule4) ((triple6) -> rule5)) -> rule3))]
Erin is cold.
("Erin" "is" "cold" "+")
triple1
Erin is round.
("Erin" "is" "round" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
((triple6) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple5
((triple6) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
((triple6) -> (rule7 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple7) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple6) -> (rule5 % int2)) triple6) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((triple6) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple6) -> (rule7 % int3)) ((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((triple7) -> (rule6 % int3)) ((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple6) -> (rule5 % int3)) triple6) -> (rule4 % int2)) ((triple6) -> (rule5 % int3))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3