Anne is kind. Anne is not young. Bob is green. Erin is green. Erin is rough. Fiona is kind. Fiona is young. If someone is kind then they are round. If Bob is young and Bob is rough then Bob is not white. If someone is white and kind then they are not smart. All green, rough people are white. If someone is round then they are rough. All green people are kind. If someone is white and not young then they are kind. If Erin is green and Erin is white then Erin is rough.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not young.
("Anne" "is" "young" "-")
Bob is green.
("Bob" "is" "green" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If someone is kind then they are round.
((("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
If Bob is young and Bob is rough then Bob is not white.
((("Bob" "is" "young" "+") ("Bob" "is" "rough" "+")) -> ("Bob" "is" "white" "-"))
If someone is white and kind then they are not smart.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "-"))
All green, rough people are white.
((("someone" "is" "green" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If someone is round then they are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
All green people are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone is white and not young then they are kind.
((("someone" "is" "white" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "kind" "+"))
If Erin is green and Erin is white then Erin is rough.
((("Erin" "is" "green" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "rough" "+"))
Fiona is kind.
True
1
proof
[(triple6)]
("Fiona" "is" "kind" "+")
triple6
Bob is not green.
False
1
inv-proof
[(triple3)]
("Bob" "is" "green" "-")
triple3
Fiona is round.
True
2
proof
[(((triple6) -> rule1))]
("Fiona" "is" "round" "+")
((triple6) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Bob is not kind.
False
2
inv-proof
[(((triple3) -> rule6))]
("Bob" "is" "kind" "-")
((triple3) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Anne is rough.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Fiona is not rough.
False
3
inv-proof
[(((((triple6) -> rule1)) -> rule5))]
("Fiona" "is" "rough" "-")
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Bob is rough.
True
4
proof
[(((((((triple3) -> rule6)) -> rule1)) -> rule5))]
("Bob" "is" "rough" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is not rough.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule1)) -> rule5))]
("Bob" "is" "rough" "-")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is white.
True
6
proof
[(((triple3 ((((((triple3) -> rule6)) -> rule1)) -> rule5)) -> rule4))]
("Bob" "is" "white" "+")
((triple3 ((((((triple3) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is not white.
False
6
inv-proof
[(((triple3 ((((((triple3) -> rule6)) -> rule1)) -> rule5)) -> rule4))]
("Bob" "is" "white" "-")
((triple3 ((((((triple3) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is not smart.
True
9
proof
[(((((triple3 ((((((triple3) -> rule6)) -> rule1)) -> rule5)) -> rule4) ((triple3) -> rule6)) -> rule3))]
("Bob" "is" "smart" "-")
((((triple3 ((((((triple3) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) ((triple3) -> (rule6 % int5))) -> (rule3 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
Bob is smart.
False
9
inv-proof
[(((((triple3 ((((((triple3) -> rule6)) -> rule1)) -> rule5)) -> rule4) ((triple3) -> rule6)) -> rule3))]
("Bob" "is" "smart" "+")
((((triple3 ((((((triple3) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) ((triple3) -> (rule6 % int5))) -> (rule3 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "white" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Anne is kind.[(triple1)] Anne is not young.[(triple2)] Bob is green.[(triple3)] Erin is green.[(triple4)] Erin is rough.[(triple5 OR ((((((triple4) -> rule6)) -> rule1)) -> rule5))] Fiona is kind.[(triple6)] Fiona is young.[(triple7)] @1: Anne is round.[(((triple1) -> rule1))] Bob is kind.[(((triple3) -> rule6))] Erin is kind.[(((triple4) -> rule6))] Erin is white.[(((triple4 triple5) -> rule4) OR ((triple4 ((((((triple4) -> rule6)) -> rule1)) -> rule5)) -> rule4))] Fiona is round.[(((triple6) -> rule1))] @2: Anne is rough.[(((((triple1) -> rule1)) -> rule5))] Bob is round.[(((((triple3) -> rule6)) -> rule1))] Erin is not smart.[(((((triple4 triple5) -> rule4) ((triple4) -> rule6)) -> rule3) OR ((((triple4 ((((((triple4) -> rule6)) -> rule1)) -> rule5)) -> rule4) ((triple4) -> rule6)) -> rule3))] Erin is round.[(((((triple4) -> rule6)) -> rule1))] Fiona is rough.[(((((triple6) -> rule1)) -> rule5))] @3: Bob is rough.[(((((((triple3) -> rule6)) -> rule1)) -> rule5))] @4: Bob is white.[(((triple3 ((((((triple3) -> rule6)) -> rule1)) -> rule5)) -> rule4))] @5: Bob is not smart.[(((((triple3 ((((((triple3) -> rule6)) -> rule1)) -> rule5)) -> rule4) ((triple3) -> rule6)) -> rule3))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is not young.
("Anne" "is" "young" "-")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
((((((triple4) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Fiona is kind.
("Fiona" "is" "kind" "+")
triple6
Fiona is young.
("Fiona" "is" "young" "+")
triple7
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple3) -> (rule6 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple4) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple4 triple5) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple4 ((((((triple4) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Fiona is round.
("Fiona" "is" "round" "+")
((triple6) -> (rule1 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Erin is not smart.
("Erin" "is" "smart" "-")
((((triple4 triple5) -> (rule4 % int3)) ((triple4) -> (rule6 % int2))) -> (rule3 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((triple4 ((((((triple4) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) ((triple4) -> (rule6 % int5))) -> (rule3 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
int5
Erin is round.
("Erin" "is" "round" "+")
((((triple4) -> (rule6 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((triple3 ((((((triple3) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is not smart.
("Bob" "is" "smart" "-")
((((triple3 ((((((triple3) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2)) ((triple3) -> (rule6 % int5))) -> (rule3 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
int4
Bob is kind.
("Bob" "is" "kind" "+")
int5