Bob is nice. Erin is cold. Harry is blue. All cold, green things are not blue. If something is big then it is not blue. If something is green and not nice then it is not blue. If something is green then it is big. All round things are big. All cold things are round. If something is green and not kind then it is cold. If Harry is not green and Harry is not round then Harry is blue.
Bob is nice.
("Bob" "is" "nice" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Harry is blue.
("Harry" "is" "blue" "+")
All cold, green things are not blue.
((("something" "is" "cold" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "-"))
If something is big then it is not blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "-"))
If something is green and not nice then it is not blue.
((("something" "is" "green" "+") ("something" "is" "nice" "~")) -> ("something" "is" "blue" "-"))
If something is green then it is big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All cold things are round.
((("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something is green and not kind then it is cold.
((("something" "is" "green" "+") ("something" "is" "kind" "~")) -> ("something" "is" "cold" "+"))
If Harry is not green and Harry is not round then Harry is blue.
((("Harry" "is" "green" "~") ("Harry" "is" "round" "~")) -> ("Harry" "is" "blue" "+"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Erin is not cold.
False
1
inv-proof
[(triple2)]
("Erin" "is" "cold" "-")
triple2
Erin is round.
True
2
proof
[(((triple2) -> rule6))]
("Erin" "is" "round" "+")
((triple2) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not round.
False
2
inv-proof
[(((triple2) -> rule6))]
("Erin" "is" "round" "-")
((triple2) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is big.
True
3
proof
[(((((triple2) -> rule6)) -> rule5))]
("Erin" "is" "big" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not big.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule5))]
("Erin" "is" "big" "-")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not blue.
True
4
proof
[(((((((triple2) -> rule6)) -> rule5)) -> rule2))]
("Erin" "is" "blue" "-")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is blue.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule5)) -> rule2))]
("Erin" "is" "blue" "+")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Harry is not round.
Unknown
inv-rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Harry" "is" "round" "-")
Bob is round.
Unknown
rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Bob" "is" "round" "+")
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "cold" "-")
Harry is big.
Unknown
rconc
[@3: Harry is big.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule7 <- FAIL)]]
("Harry" "is" "big" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Bob is nice.[(triple1)] Erin is cold.[(triple2)] Harry is blue.[(triple3)] @1: Erin is round.[(((triple2) -> rule6))] @2: Erin is big.[(((((triple2) -> rule6)) -> rule5))] @3: Erin is not blue.[(((((((triple2) -> rule6)) -> rule5)) -> rule2))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
triple3
Erin is round.
("Erin" "is" "round" "+")
((triple2) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
((((triple2) -> (rule6 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
((((((triple2) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3