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