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