Erin is blue. Fiona is blue. Harry is cold. All cold people are red. If someone is kind and big then they are red. Cold people are red. If someone is round then they are big. If someone is nice then they are round. If someone is red then they are round.
Erin is blue.
("Erin" "is" "blue" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
All cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is kind and big then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone is round then they are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is nice then they are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is red then they are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
Erin is blue.
True
1
proof
[(triple1)]
("Erin" "is" "blue" "+")
triple1
Erin is not blue.
False
1
inv-proof
[(triple1)]
("Erin" "is" "blue" "-")
triple1
Harry is red.
True
2
proof
[(((triple3) -> rule1) OR ((triple3) -> rule3))]
("Harry" "is" "red" "+")
((triple3) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple3) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple3) -> rule1) OR ((triple3) -> rule3))]
("Harry" "is" "red" "-")
((triple3) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple3) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
True
3
proof
[(((((triple3) -> rule1)) -> rule6) OR ((((triple3) -> rule3)) -> rule6))]
("Harry" "is" "round" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not round.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule6) OR ((((triple3) -> rule3)) -> rule6))]
("Harry" "is" "round" "-")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
True
4
proof
[(((((((triple3) -> rule1)) -> rule6)) -> rule4) OR ((((((triple3) -> rule3)) -> rule6)) -> rule4))]
("Harry" "is" "big" "+")
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not big.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule6)) -> rule4) OR ((((((triple3) -> rule3)) -> rule6)) -> rule4))]
("Harry" "is" "big" "-")
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Erin is not round.
Unknown
inv-rconc
[@2: Erin is round.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Erin" "is" "round" "-")
Fiona is big.
Unknown
rconc
[@3: Fiona is big.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule1 <- FAIL)]]
("Fiona" "is" "big" "+")
Erin is not red.
Unknown
inv-rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "red" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "red" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
@0: Erin is blue.[(triple1)] Fiona is blue.[(triple2)] Harry is cold.[(triple3)] @1: Harry is red.[(((triple3) -> rule1) OR ((triple3) -> rule3))] @2: Harry is round.[(((((triple3) -> rule1)) -> rule6) OR ((((triple3) -> rule3)) -> rule6))] @3: Harry is big.[(((((((triple3) -> rule1)) -> rule6)) -> rule4) OR ((((((triple3) -> rule3)) -> rule6)) -> rule4))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple2
Harry is cold.
("Harry" "is" "cold" "+")
triple3
Harry is red.
("Harry" "is" "red" "+")
((triple3) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple3) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((((triple3) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3