Bob is red. Erin is red. Harry is quiet. Round people are blue. Rough people are white. If Harry is red and Harry is quiet then Harry is round. Red people are rough. If Erin is blue and Erin is white then Erin is rough. If Erin is white then Erin is round.
Bob is red.
("Bob" "is" "red" "+")
Erin is red.
("Erin" "is" "red" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Round people are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If Harry is red and Harry is quiet then Harry is round.
((("Harry" "is" "red" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "round" "+"))
Red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If Erin is blue and Erin is white then Erin is rough.
((("Erin" "is" "blue" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "rough" "+"))
If Erin is white then Erin is round.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "round" "+"))
Harry is quiet.
True
1
proof
[(triple3)]
("Harry" "is" "quiet" "+")
triple3
Erin is not red.
False
1
inv-proof
[(triple2)]
("Erin" "is" "red" "-")
triple2
Bob is rough.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Erin is not rough.
False
2
inv-proof
[(((triple2) -> rule4))]
("Erin" "is" "rough" "-")
((triple2) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
True
3
proof
[(((((triple2) -> rule4)) -> rule2))]
("Erin" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not white.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule2))]
("Erin" "is" "white" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
True
4
proof
[(((((((triple2) -> rule4)) -> rule2)) -> rule6))]
("Erin" "is" "round" "+")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not round.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule2)) -> rule6))]
("Erin" "is" "round" "-")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "blue" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "rough" "+")
Harry is not blue.
Unknown
inv-rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Harry" "is" "blue" "-")
Harry is white.
Unknown
rconc
[@2: Harry is white.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Harry" "is" "white" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is red.[(triple1)] Erin is red.[(triple2)] Harry is quiet.[(triple3)] @1: Bob is rough.[(((triple1) -> rule4))] Erin is rough.[(((triple2) -> rule4))] @2: Bob is white.[(((((triple1) -> rule4)) -> rule2))] Erin is white.[(((((triple2) -> rule4)) -> rule2))] @3: Erin is round.[(((((((triple2) -> rule4)) -> rule2)) -> rule6))] @4: Erin is blue.[(((((((((triple2) -> rule4)) -> rule2)) -> rule6)) -> rule1))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple2) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
((((((((triple2) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4