Bob is not blue. Bob is cold. Bob is kind. Charlie is cold. Charlie is green. Gary is kind. Harry is green. Green people are blue. All green, red people are not nice. If someone is blue and not green then they are not cold. If someone is rough then they are cold. If Bob is blue and Bob is cold then Bob is kind. All blue people are rough. All cold people are red. Nice, blue people are kind. If Gary is not rough then Gary is nice.
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is green.
("Harry" "is" "green" "+")
Green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
All green, red people are not nice.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "-"))
If someone is blue and not green then they are not cold.
((("someone" "is" "blue" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "cold" "-"))
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If Bob is blue and Bob is cold then Bob is kind.
((("Bob" "is" "blue" "+") ("Bob" "is" "cold" "+")) -> ("Bob" "is" "kind" "+"))
All blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
All cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
Nice, blue people are kind.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If Gary is not rough then Gary is nice.
((("Gary" "is" "rough" "~")) -> ("Gary" "is" "nice" "+"))
Charlie is cold.
True
1
proof
[(triple4 OR ((((((triple5) -> rule1)) -> rule6)) -> rule4))]
("Charlie" "is" "cold" "+")
triple4
((((((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Gary is not kind.
False
1
inv-proof
[(triple6)]
("Gary" "is" "kind" "-")
triple6
Charlie is red.
True
2
proof
[(((triple4) -> rule7) OR ((((((((triple5) -> rule1)) -> rule6)) -> rule4)) -> rule7))]
("Charlie" "is" "red" "+")
((triple4) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((((((triple5) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is not red.
False
2
inv-proof
[(((triple4) -> rule7) OR ((((((((triple5) -> rule1)) -> rule6)) -> rule4)) -> rule7))]
("Charlie" "is" "red" "-")
((triple4) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((((((triple5) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is rough.
True
3
proof
[(((((triple5) -> rule1)) -> rule6))]
("Charlie" "is" "rough" "+")
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is nice.
False
4
inv-proof
[(((triple5 ((triple4) -> rule7)) -> rule2) OR ((triple5 ((((((((triple5) -> rule1)) -> rule6)) -> rule4)) -> rule7)) -> rule2))]
("Charlie" "is" "nice" "+")
((triple5 ((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((triple5 ((((((((triple5) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is blue.
("Charlie" "is" "blue" "+")
int5
Harry is cold.
True
4
proof
[(((((((triple7) -> rule1)) -> rule6)) -> rule4))]
("Harry" "is" "cold" "+")
((((((triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not cold.
False
4
inv-proof
[(((((((triple7) -> rule1)) -> rule6)) -> rule4))]
("Harry" "is" "cold" "-")
((((((triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is red.
True
5
proof
[(((((((((triple7) -> rule1)) -> rule6)) -> rule4)) -> rule7))]
("Harry" "is" "red" "+")
((((((((triple7) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is not red.
False
5
inv-proof
[(((((((((triple7) -> rule1)) -> rule6)) -> rule4)) -> rule7))]
("Harry" "is" "red" "-")
((((((((triple7) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is not nice.
True
7
proof
[(((triple7 ((((((((triple7) -> rule1)) -> rule6)) -> rule4)) -> rule7)) -> rule2))]
("Harry" "is" "nice" "-")
((triple7 ((((((((triple7) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is blue.
("Harry" "is" "blue" "+")
int5
Harry is nice.
False
7
inv-proof
[(((triple7 ((((((((triple7) -> rule1)) -> rule6)) -> rule4)) -> rule7)) -> rule2))]
("Harry" "is" "nice" "+")
((triple7 ((((((((triple7) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is blue.
("Harry" "is" "blue" "+")
int5
Gary is not rough.
Unknown
inv-rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Gary" "is" "rough" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "kind" "+")
Gary is not red.
Unknown
inv-rconc
[@4: Gary is red.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule6 <- rule1 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "blue" "+")
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Gary" "is" "nice" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is cold.[(triple2)] Bob is kind.[(triple3)] Bob is not blue.[(triple1)] Charlie is cold.[(triple4 OR ((((((triple5) -> rule1)) -> rule6)) -> rule4))] Charlie is green.[(triple5)] Gary is kind.[(triple6)] Harry is green.[(triple7)] @1: Bob is red.[(((triple2) -> rule7))] Charlie is blue.[(((triple5) -> rule1))] Charlie is red.[(((triple4) -> rule7) OR ((((((((triple5) -> rule1)) -> rule6)) -> rule4)) -> rule7))] Harry is blue.[(((triple7) -> rule1))] @2: Charlie is not nice.[(((triple5 ((triple4) -> rule7)) -> rule2) OR ((triple5 ((((((((triple5) -> rule1)) -> rule6)) -> rule4)) -> rule7)) -> rule2))] Charlie is rough.[(((((triple5) -> rule1)) -> rule6))] Harry is rough.[(((((triple7) -> rule1)) -> rule6))] @3: Harry is cold.[(((((((triple7) -> rule1)) -> rule6)) -> rule4))] @4: Harry is red.[(((((((((triple7) -> rule1)) -> rule6)) -> rule4)) -> rule7))] @5: Harry is not nice.[(((triple7 ((((((((triple7) -> rule1)) -> rule6)) -> rule4)) -> rule7)) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is not blue.
("Bob" "is" "blue" "-")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple4
((((((triple5) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
Bob is red.
("Bob" "is" "red" "+")
((triple2) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple5) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple4) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((((((triple5) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Harry is blue.
("Harry" "is" "blue" "+")
((triple7) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Charlie is not nice.
("Charlie" "is" "nice" "-")
((triple5 ((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((triple5 ((((((((triple5) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is blue.
("Charlie" "is" "blue" "+")
int5
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
((((((((triple7) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
int4
Harry is not nice.
("Harry" "is" "nice" "-")
((triple7 ((((((((triple7) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Harry is not nice.
("Harry" "is" "nice" "-")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is blue.
("Harry" "is" "blue" "+")
int5