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