Bob is cold. Dave is smart. Erin is cold. Harry is not cold. If someone is cold then they are green. If someone is green and blue then they are not nice. If someone is green then they are blue. All green people are rough. If someone is green and not blue then they are quiet. If someone is cold and not rough then they are smart. Cold, nice people are smart. If someone is green and not blue then they are smart.
Bob is cold.
("Bob" "is" "cold" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
If someone is cold then they are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is green and blue then they are not nice.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "-"))
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
All green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is green and not blue then they are quiet.
((("someone" "is" "green" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "quiet" "+"))
If someone is cold and not rough then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "smart" "+"))
Cold, nice people are smart.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is green and not blue then they are smart.
((("someone" "is" "green" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "smart" "+"))
Erin is cold.
True
1
proof
[(triple3)]
("Erin" "is" "cold" "+")
triple3
Harry is cold.
False
1
inv-proof
[(triple4)]
("Harry" "is" "cold" "+")
triple4
Erin is green.
True
2
proof
[(((triple3) -> rule1))]
("Erin" "is" "green" "+")
((triple3) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple3) -> rule1))]
("Erin" "is" "green" "-")
((triple3) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Bob is rough.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("Bob" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Erin is not blue.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule3))]
("Erin" "is" "blue" "-")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not nice.
True
6
proof
[(((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule3)) -> rule2))]
("Erin" "is" "nice" "-")
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Bob is nice.
False
6
inv-proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule2))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "smart" "+")
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "smart" "-")
Dave is rough.
Unknown
rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Dave" "is" "rough" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Bob is cold.[(triple1)] Dave is smart.[(triple2)] Erin is cold.[(triple3)] Harry is not cold.[(triple4)] @1: Bob is green.[(((triple1) -> rule1))] Erin is green.[(((triple3) -> rule1))] @2: Bob is blue.[(((((triple1) -> rule1)) -> rule3))] Bob is rough.[(((((triple1) -> rule1)) -> rule4))] Erin is blue.[(((((triple3) -> rule1)) -> rule3))] Erin is rough.[(((((triple3) -> rule1)) -> rule4))] @3: Bob is not nice.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule2))] Erin is not nice.[(((((triple3) -> rule1) ((((triple3) -> rule1)) -> rule3)) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Harry is not cold.
("Harry" "is" "cold" "-")
triple4
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Bob is not nice.
("Bob" "is" "nice" "-")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Erin is not nice.
("Erin" "is" "nice" "-")
((((triple3) -> (rule1 % int3)) ((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is not nice.
("Erin" "is" "nice" "-")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3