Bob is not cold. Bob is kind. Bob is not round. Bob is smart. Charlie is rough. Charlie is round. Charlie is smart. Dave is nice. Dave is rough. Dave is round. Erin is not cold. Erin is rough. All cold, nice people are not rough. Nice, kind people are not blue. If Dave is blue and Dave is not cold then Dave is smart. If someone is blue then they are smart. If someone is rough then they are smart. If Bob is not round then Bob is rough. If someone is kind and smart then they are nice. All round people are kind.
Bob is not cold.
("Bob" "is" "cold" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not round.
("Bob" "is" "round" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is rough.
("Erin" "is" "rough" "+")
All cold, nice people are not rough.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "-"))
Nice, kind people are not blue.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "-"))
If Dave is blue and Dave is not cold then Dave is smart.
((("Dave" "is" "blue" "+") ("Dave" "is" "cold" "~")) -> ("Dave" "is" "smart" "+"))
If someone is blue then they are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If someone is rough then they are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If Bob is not round then Bob is rough.
((("Bob" "is" "round" "~")) -> ("Bob" "is" "rough" "+"))
If someone is kind and smart then they are nice.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
All round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Bob is not cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "-")
triple1
Charlie is not rough.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "rough" "-")
triple5
Bob is rough.
True
2
proof
[(((triple3) -> rule6))]
("Bob" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple9) -> rule5))]
("Dave" "is" "smart" "-")
((triple9) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Charlie is nice.
True
4
proof
[(((((triple6) -> rule8) triple7) -> rule7) OR ((((triple6) -> rule8) ((triple5) -> rule5)) -> rule7))]
("Charlie" "is" "nice" "+")
((((triple6) -> (rule8 % int2)) triple7) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple6) -> (rule8 % int3)) ((triple5) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Dave is blue.
False
4
inv-proof
[(((triple8 ((triple10) -> rule8)) -> rule2) OR ((((((triple10) -> rule8) ((triple9) -> rule5)) -> rule7) ((triple10) -> rule8)) -> rule2))]
("Dave" "is" "blue" "+")
((triple8 ((triple10) -> (rule8 % int2))) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((((triple10) -> (rule8 % int4)) ((triple9) -> (rule5 % int3))) -> (rule7 % int2)) ((triple10) -> (rule8 % int4))) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Charlie is not blue.
True
7
proof
[(((((((triple6) -> rule8) triple7) -> rule7) ((triple6) -> rule8)) -> rule2) OR ((((((triple6) -> rule8) ((triple5) -> rule5)) -> rule7) ((triple6) -> rule8)) -> rule2))]
("Charlie" "is" "blue" "-")
((((((triple6) -> (rule8 % int3)) triple7) -> (rule7 % int2)) ((triple6) -> (rule8 % int3))) -> (rule2 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple6) -> (rule8 % int4)) ((triple5) -> (rule5 % int3))) -> (rule7 % int2)) ((triple6) -> (rule8 % int4))) -> (rule2 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Charlie is blue.
False
7
inv-proof
[(((((((triple6) -> rule8) triple7) -> rule7) ((triple6) -> rule8)) -> rule2) OR ((((((triple6) -> rule8) ((triple5) -> rule5)) -> rule7) ((triple6) -> rule8)) -> rule2))]
("Charlie" "is" "blue" "+")
((((((triple6) -> (rule8 % int3)) triple7) -> (rule7 % int2)) ((triple6) -> (rule8 % int3))) -> (rule2 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple6) -> (rule8 % int4)) ((triple5) -> (rule5 % int3))) -> (rule7 % int2)) ((triple6) -> (rule8 % int4))) -> (rule2 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4
Erin is not nice.
Unknown
inv-rconc
[@2: Erin is nice.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "kind" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Bob is kind.[(triple2)] Bob is not cold.[(triple1)] Bob is not round.[(triple3)] Bob is smart.[(triple4 OR ((((triple3) -> rule6)) -> rule5))] Charlie is rough.[(triple5)] Charlie is round.[(triple6)] Charlie is smart.[(triple7 OR ((triple5) -> rule5))] Dave is nice.[(triple8 OR ((((triple10) -> rule8) ((triple9) -> rule5)) -> rule7))] Dave is rough.[(triple9)] Dave is round.[(triple10)] Erin is not cold.[(triple11)] Erin is rough.[(triple12)] @1: Bob is nice.[(((triple2 triple4) -> rule7) OR ((triple2 ((((triple3) -> rule6)) -> rule5)) -> rule7))] Bob is rough.[(((triple3) -> rule6))] Charlie is kind.[(((triple6) -> rule8))] Dave is kind.[(((triple10) -> rule8))] Dave is smart.[(((triple9) -> rule5))] Erin is smart.[(((triple12) -> rule5))] @2: Bob is not blue.[(((((triple2 triple4) -> rule7) triple2) -> rule2) OR ((((triple2 ((((triple3) -> rule6)) -> rule5)) -> rule7) triple2) -> rule2))] Charlie is nice.[(((((triple6) -> rule8) triple7) -> rule7) OR ((((triple6) -> rule8) ((triple5) -> rule5)) -> rule7))] Dave is not blue.[(((triple8 ((triple10) -> rule8)) -> rule2) OR ((((((triple10) -> rule8) ((triple9) -> rule5)) -> rule7) ((triple10) -> rule8)) -> rule2))] @3: Charlie is not blue.[(((((((triple6) -> rule8) triple7) -> rule7) ((triple6) -> rule8)) -> rule2) OR ((((((triple6) -> rule8) ((triple5) -> rule5)) -> rule7) ((triple6) -> rule8)) -> rule2))]
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is not cold.
("Bob" "is" "cold" "-")
triple1
Bob is not round.
("Bob" "is" "round" "-")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
((((triple3) -> (rule6 % int2))) -> (rule5 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
((triple5) -> (rule5 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple8
((((triple10) -> (rule8 % int3)) ((triple9) -> (rule5 % int2))) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
triple9
Dave is round.
("Dave" "is" "round" "+")
triple10
Erin is not cold.
("Erin" "is" "cold" "-")
triple11
Erin is rough.
("Erin" "is" "rough" "+")
triple12
Bob is nice.
("Bob" "is" "nice" "+")
((triple2 triple4) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple2 ((((triple3) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple6) -> (rule8 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((triple10) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple9) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple12) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Bob is not blue.
("Bob" "is" "blue" "-")
((((triple2 triple4) -> (rule7 % int2)) triple2) -> (rule2 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((triple2 ((((triple3) -> (rule6 % int4))) -> (rule5 % int3))) -> (rule7 % int2)) triple2) -> (rule2 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple6) -> (rule8 % int2)) triple7) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((triple6) -> (rule8 % int3)) ((triple5) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Dave is not blue.
("Dave" "is" "blue" "-")
((triple8 ((triple10) -> (rule8 % int2))) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((((triple10) -> (rule8 % int4)) ((triple9) -> (rule5 % int3))) -> (rule7 % int2)) ((triple10) -> (rule8 % int4))) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Charlie is not blue.
("Charlie" "is" "blue" "-")
((((((triple6) -> (rule8 % int3)) triple7) -> (rule7 % int2)) ((triple6) -> (rule8 % int3))) -> (rule2 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
((((((triple6) -> (rule8 % int4)) ((triple5) -> (rule5 % int3))) -> (rule7 % int2)) ((triple6) -> (rule8 % int4))) -> (rule2 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
int4