Anne is white. Bob is white. Erin is white. Gary is big. All smart people are green. If someone is big and smart then they are young. All young people are white. If someone is green and white then they are big. All smart people are young. All smart, young people are white. All big people are smart. All white, blue people are green.
Anne is white.
("Anne" "is" "white" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is big.
("Gary" "is" "big" "+")
All smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is big and smart then they are young.
((("someone" "is" "big" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
All young people are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If someone is green and white then they are big.
((("someone" "is" "green" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
All smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
All smart, young people are white.
((("someone" "is" "smart" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
All big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
All white, blue people are green.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Erin is white.
True
1
proof
[(triple3)]
("Erin" "is" "white" "+")
triple3
Erin is not white.
False
1
inv-proof
[(triple3)]
("Erin" "is" "white" "-")
triple3
Gary is smart.
True
2
proof
[(((triple4) -> rule7))]
("Gary" "is" "smart" "+")
((triple4) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple4) -> rule7))]
("Gary" "is" "smart" "-")
((triple4) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
True
3
proof
[(((((triple4) -> rule7)) -> rule5) OR ((triple4 ((triple4) -> rule7)) -> rule2))]
("Gary" "is" "young" "+")
((((triple4) -> (rule7 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((triple4 ((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple4) -> rule7)) -> rule1))]
("Gary" "is" "green" "-")
((((triple4) -> (rule7 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
True
4
proof
[(((((((triple4) -> rule7)) -> rule5)) -> rule3) OR ((((triple4 ((triple4) -> rule7)) -> rule2)) -> rule3) OR ((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule5)) -> rule6) OR ((((triple4) -> rule7) ((triple4 ((triple4) -> rule7)) -> rule2)) -> rule6))]
("Gary" "is" "white" "+")
((((((triple4) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple4 ((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple4) -> (rule7 % int3)) ((((triple4) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple4) -> (rule7 % int3)) ((triple4 ((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not white.
False
4
inv-proof
[(((((((triple4) -> rule7)) -> rule5)) -> rule3) OR ((((triple4 ((triple4) -> rule7)) -> rule2)) -> rule3) OR ((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule5)) -> rule6) OR ((((triple4) -> rule7) ((triple4 ((triple4) -> rule7)) -> rule2)) -> rule6))]
("Gary" "is" "white" "-")
((((((triple4) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple4 ((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple4) -> (rule7 % int3)) ((((triple4) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple4) -> (rule7 % int3)) ((triple4 ((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Bob is not smart.
Unknown
inv-rconc
[@3: Bob is smart.[CWA. Example of deepest failure = (rule7 <- rule4 <- rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Erin is green.
Unknown
rconc
[@4: Erin is green.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule4 <- rule8 <- FAIL)]]
("Erin" "is" "green" "+")
Bob is not green.
Unknown
inv-rconc
[@4: Bob is green.[CWA. Example of deepest failure = (rule1 <- rule7 <- rule4 <- rule8 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is young.
Unknown
rconc
[@4: Bob is young.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule1 <- rule7 <- FAIL)]]
("Bob" "is" "young" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is white.[(triple1)] Bob is white.[(triple2)] Erin is white.[(triple3)] Gary is big.[(triple4)] @1: Gary is smart.[(((triple4) -> rule7))] @2: Gary is green.[(((((triple4) -> rule7)) -> rule1))] Gary is young.[(((((triple4) -> rule7)) -> rule5) OR ((triple4 ((triple4) -> rule7)) -> rule2))] @3: Gary is white.[(((((((triple4) -> rule7)) -> rule5)) -> rule3) OR ((((triple4 ((triple4) -> rule7)) -> rule2)) -> rule3) OR ((((triple4) -> rule7) ((((triple4) -> rule7)) -> rule5)) -> rule6) OR ((((triple4) -> rule7) ((triple4 ((triple4) -> rule7)) -> rule2)) -> rule6))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Gary is big.
("Gary" "is" "big" "+")
triple4
Gary is smart.
("Gary" "is" "smart" "+")
((triple4) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((((triple4) -> (rule7 % int2))) -> (rule1 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((((triple4) -> (rule7 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
((triple4 ((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((((triple4) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple4 ((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple4) -> (rule7 % int3)) ((((triple4) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
((((triple4) -> (rule7 % int3)) ((triple4 ((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3