Anne is green. Bob is rough. Erin is furry. Harry is round. If something is green then it is red. If something is big and not round then it is red. Furry things are green. If something is green and furry then it is rough. All red, rough things are big. If Anne is big then Anne is red.
Anne is green.
("Anne" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is green then it is red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
If something is big and not round then it is red.
((("something" "is" "big" "+") ("something" "is" "round" "~")) -> ("something" "is" "red" "+"))
Furry things are green.
((("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If something is green and furry then it is rough.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
All red, rough things are big.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If Anne is big then Anne is red.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "red" "+"))
Harry is round.
True
1
proof
[(triple4)]
("Harry" "is" "round" "+")
triple4
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Erin is green.
True
2
proof
[(((triple3) -> rule3))]
("Erin" "is" "green" "+")
((triple3) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple3) -> rule3))]
("Erin" "is" "green" "-")
((triple3) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
True
3
proof
[(((((triple3) -> rule3)) -> rule1))]
("Erin" "is" "red" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not red.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule1))]
("Erin" "is" "red" "-")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
True
8
proof
[(((((((triple3) -> rule3)) -> rule1) ((((triple3) -> rule3) triple3) -> rule4)) -> rule5))]
("Erin" "is" "big" "+")
((((((triple3) -> (rule3 % int4))) -> (rule1 % int3)) ((((triple3) -> (rule3 % int4)) triple3) -> (rule4 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is not big.
False
8
inv-proof
[(((((((triple3) -> rule3)) -> rule1) ((((triple3) -> rule3) triple3) -> rule4)) -> rule5))]
("Erin" "is" "big" "-")
((((((triple3) -> (rule3 % int4))) -> (rule1 % int3)) ((((triple3) -> (rule3 % int4)) triple3) -> (rule4 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "green" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "rough" "+")
Bob is not red.
Unknown
inv-rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Bob" "is" "red" "-")
Bob is big.
Unknown
rconc
[@3: Bob is big.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule3 <- FAIL)]]
("Bob" "is" "big" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Anne is green.[(triple1)] Bob is rough.[(triple2)] Erin is furry.[(triple3)] Harry is round.[(triple4)] @1: Anne is red.[(((triple1) -> rule1))] Erin is green.[(((triple3) -> rule3))] @2: Erin is red.[(((((triple3) -> rule3)) -> rule1))] Erin is rough.[(((((triple3) -> rule3) triple3) -> rule4))] @3: Erin is big.[(((((((triple3) -> rule3)) -> rule1) ((((triple3) -> rule3) triple3) -> rule4)) -> rule5))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple3) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((((triple3) -> (rule3 % int4))) -> (rule1 % int3)) ((((triple3) -> (rule3 % int4)) triple3) -> (rule4 % int2))) -> (rule5 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4