Bob is big. Bob is not blue. Dave is blue. Dave is rough. Dave is white. Erin is cold. Erin is white. Cold, white things are green. If something is big then it is cold. All blue things are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is not blue.
("Bob" "is" "blue" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is white.
("Erin" "is" "white" "+")
Cold, white things are green.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If something is big then it is cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Erin is cold.
True
1
proof
[(triple6)]
("Erin" "is" "cold" "+")
triple6
Erin is not white.
False
1
inv-proof
[(triple7)]
("Erin" "is" "white" "-")
triple7
Dave is big.
True
2
proof
[(((triple3) -> rule3))]
("Dave" "is" "big" "+")
((triple3) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "cold" "-")
((triple1) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Dave is cold.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("Dave" "is" "cold" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not cold.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("Dave" "is" "cold" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is green.
True
5
proof
[(((((((triple3) -> rule3)) -> rule2) triple5) -> rule1))]
("Dave" "is" "green" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not green.
False
5
inv-proof
[(((((((triple3) -> rule3)) -> rule2) triple5) -> rule1))]
("Dave" "is" "green" "-")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "big" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
@0: Bob is big.[(triple1)] Bob is not blue.[(triple2)] Dave is blue.[(triple3)] Dave is rough.[(triple4)] Dave is white.[(triple5)] Erin is cold.[(triple6)] Erin is white.[(triple7)] @1: Bob is cold.[(((triple1) -> rule2))] Dave is big.[(((triple3) -> rule3))] Erin is green.[(((triple6 triple7) -> rule1))] @2: Dave is cold.[(((((triple3) -> rule3)) -> rule2))] @3: Dave is green.[(((((((triple3) -> rule3)) -> rule2) triple5) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is not blue.
("Bob" "is" "blue" "-")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple3) -> (rule3 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple6 triple7) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2)) triple5) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3