Bob is cold. Bob is nice. Bob is red. Bob is young. Dave is cold. Dave is red. Erin is not cold. Erin is red. Erin is young. Gary is kind. Red, cold people are rough. If someone is red and not nice then they are cold. If Erin is kind then Erin is rough. If someone is kind then they are not blue. Rough people are blue. If someone is nice and young then they are red. Blue people are not kind. Nice, blue people are not kind.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Red, cold people are rough.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone is red and not nice then they are cold.
((("someone" "is" "red" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "cold" "+"))
If Erin is kind then Erin is rough.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "rough" "+"))
If someone is kind then they are not blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "-"))
Rough people are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If someone is nice and young then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
Blue people are not kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "-"))
Nice, blue people are not kind.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "-"))
Gary is kind.
True
1
proof
[(triple10)]
("Gary" "is" "kind" "+")
triple10
Dave is not cold.
False
1
inv-proof
[(triple5)]
("Dave" "is" "cold" "-")
triple5
Gary is not blue.
True
2
proof
[(((triple10) -> rule4))]
("Gary" "is" "blue" "-")
((triple10) -> (rule4 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Bob is not rough.
False
3
inv-proof
[(((triple3 triple1) -> rule1) OR ((((triple2 triple4) -> rule6) triple1) -> rule1))]
("Bob" "is" "rough" "-")
((triple3 triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple2 triple4) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is blue.
True
4
proof
[(((((triple3 triple1) -> rule1)) -> rule5) OR ((((((triple2 triple4) -> rule6) triple1) -> rule1)) -> rule5))]
("Bob" "is" "blue" "+")
((((triple3 triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple2 triple4) -> (rule6 % int3)) triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not blue.
False
4
inv-proof
[(((((triple3 triple1) -> rule1)) -> rule5) OR ((((((triple2 triple4) -> rule6) triple1) -> rule1)) -> rule5))]
("Bob" "is" "blue" "-")
((((triple3 triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple2 triple4) -> (rule6 % int3)) triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not kind.
True
5
proof
[(((((((triple3 triple1) -> rule1)) -> rule5)) -> rule7) OR ((triple2 ((((triple3 triple1) -> rule1)) -> rule5)) -> rule8) OR ((((((((triple2 triple4) -> rule6) triple1) -> rule1)) -> rule5)) -> rule7) OR ((triple2 ((((((triple2 triple4) -> rule6) triple1) -> rule1)) -> rule5)) -> rule8))]
("Bob" "is" "kind" "-")
((((((triple3 triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((triple2 ((((triple3 triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((((((triple2 triple4) -> (rule6 % int4)) triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
((triple2 ((((((triple2 triple4) -> (rule6 % int4)) triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Dave is kind.
False
5
inv-proof
[(((((((triple6 triple5) -> rule1)) -> rule5)) -> rule7))]
("Dave" "is" "kind" "+")
((((((triple6 triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Gary is not rough.
Unknown
inv-rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("Gary" "is" "rough" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "red" "+")
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is blue.
Unknown
rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Erin" "is" "blue" "+")
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" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Bob is cold.[(triple1)] Bob is nice.[(triple2)] Bob is red.[(triple3 OR ((triple2 triple4) -> rule6))] Bob is young.[(triple4)] Dave is cold.[(triple5)] Dave is red.[(triple6)] Erin is not cold.[(triple7)] Erin is red.[(triple8)] Erin is young.[(triple9)] Gary is kind.[(triple10)] @1: Bob is rough.[(((triple3 triple1) -> rule1) OR ((((triple2 triple4) -> rule6) triple1) -> rule1))] Dave is rough.[(((triple6 triple5) -> rule1))] Gary is not blue.[(((triple10) -> rule4))] @2: Bob is blue.[(((((triple3 triple1) -> rule1)) -> rule5) OR ((((((triple2 triple4) -> rule6) triple1) -> rule1)) -> rule5))] Dave is blue.[(((((triple6 triple5) -> rule1)) -> rule5))] @3: Bob is not kind.[(((((((triple3 triple1) -> rule1)) -> rule5)) -> rule7) OR ((triple2 ((((triple3 triple1) -> rule1)) -> rule5)) -> rule8) OR ((((((((triple2 triple4) -> rule6) triple1) -> rule1)) -> rule5)) -> rule7) OR ((triple2 ((((((triple2 triple4) -> rule6) triple1) -> rule1)) -> rule5)) -> rule8))] Dave is not kind.[(((((((triple6 triple5) -> rule1)) -> rule5)) -> rule7))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
((triple2 triple4) -> (rule6 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is red.
("Dave" "is" "red" "+")
triple6
Erin is not cold.
("Erin" "is" "cold" "-")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple8
Erin is young.
("Erin" "is" "young" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
Bob is rough.
("Bob" "is" "rough" "+")
((triple3 triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple2 triple4) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((triple6 triple5) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Gary is not blue.
("Gary" "is" "blue" "-")
((triple10) -> (rule4 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple3 triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple2 triple4) -> (rule6 % int3)) triple1) -> (rule1 % int2))) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
((((triple6 triple5) -> (rule1 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Bob is not kind.
("Bob" "is" "kind" "-")
((((((triple3 triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((triple2 ((((triple3 triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
((((((((triple2 triple4) -> (rule6 % int4)) triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
((triple2 ((((((triple2 triple4) -> (rule6 % int4)) triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
int4
Dave is not kind.
("Dave" "is" "kind" "-")
((((((triple6 triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3