Anne is furry. Anne is green. Anne is young. Bob is green. Bob is round. Fiona is round. Gary is furry. Young things are big. White things are green. All smart, young things are white. If something is smart then it is young. If something is young and green then it is round. If Gary is furry then Gary is smart.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is round.
("Bob" "is" "round" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
White things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
All smart, young things are white.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If something is smart then it is young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If something is young and green then it is round.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If Gary is furry then Gary is smart.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "smart" "+"))
Fiona is round.
True
1
proof
[(triple6)]
("Fiona" "is" "round" "+")
triple6
Fiona is not round.
False
1
inv-proof
[(triple6)]
("Fiona" "is" "round" "-")
triple6
Gary is smart.
True
2
proof
[(((triple7) -> rule6))]
("Gary" "is" "smart" "+")
((triple7) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Anne is not round.
False
3
inv-proof
[(((triple3 triple2) -> rule5))]
("Anne" "is" "round" "-")
((triple3 triple2) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Gary is young.
True
3
proof
[(((((triple7) -> rule6)) -> rule4))]
("Gary" "is" "young" "+")
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not young.
False
3
inv-proof
[(((((triple7) -> rule6)) -> rule4))]
("Gary" "is" "young" "-")
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
True
6
proof
[(((((triple7) -> rule6) ((((triple7) -> rule6)) -> rule4)) -> rule3))]
("Gary" "is" "white" "+")
((((triple7) -> (rule6 % int3)) ((((triple7) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % 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
6
inv-proof
[(((((triple7) -> rule6) ((((triple7) -> rule6)) -> rule4)) -> rule3))]
("Gary" "is" "white" "-")
((((triple7) -> (rule6 % int3)) ((((triple7) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is green.
True
7
proof
[(((((((triple7) -> rule6) ((((triple7) -> rule6)) -> rule4)) -> rule3)) -> rule2))]
("Gary" "is" "green" "+")
((((((triple7) -> (rule6 % int4)) ((((triple7) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is not green.
False
7
inv-proof
[(((((((triple7) -> rule6) ((((triple7) -> rule6)) -> rule4)) -> rule3)) -> rule2))]
("Gary" "is" "green" "-")
((((((triple7) -> (rule6 % int4)) ((((triple7) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is round.
True
11
proof
[(((((((triple7) -> rule6)) -> rule4) ((((((triple7) -> rule6) ((((triple7) -> rule6)) -> rule4)) -> rule3)) -> rule2)) -> rule5))]
("Gary" "is" "round" "+")
((((((triple7) -> (rule6 % int5))) -> (rule4 % int4)) ((((((triple7) -> (rule6 % int5)) ((((triple7) -> (rule6 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Gary is not round.
False
11
inv-proof
[(((((((triple7) -> rule6)) -> rule4) ((((((triple7) -> rule6) ((((triple7) -> rule6)) -> rule4)) -> rule3)) -> rule2)) -> rule5))]
("Gary" "is" "round" "-")
((((((triple7) -> (rule6 % int5))) -> (rule4 % int4)) ((((((triple7) -> (rule6 % int5)) ((((triple7) -> (rule6 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Bob is not big.
Unknown
inv-rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Bob" "is" "big" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "white" "+")
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "white" "-")
Fiona is big.
Unknown
rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "young" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "young" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Anne is green.[(triple2)] Anne is young.[(triple3)] Bob is green.[(triple4)] Bob is round.[(triple5)] Fiona is round.[(triple6)] Gary is furry.[(triple7)] @1: Anne is big.[(((triple3) -> rule1))] Anne is round.[(((triple3 triple2) -> rule5))] Gary is smart.[(((triple7) -> rule6))] @2: Gary is young.[(((((triple7) -> rule6)) -> rule4))] @3: Gary is big.[(((((((triple7) -> rule6)) -> rule4)) -> rule1))] Gary is white.[(((((triple7) -> rule6) ((((triple7) -> rule6)) -> rule4)) -> rule3))] @4: Gary is green.[(((((((triple7) -> rule6) ((((triple7) -> rule6)) -> rule4)) -> rule3)) -> rule2))] @5: Gary is round.[(((((((triple7) -> rule6)) -> rule4) ((((((triple7) -> rule6) ((((triple7) -> rule6)) -> rule4)) -> rule3)) -> rule2)) -> rule5))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Fiona is round.
("Fiona" "is" "round" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple3 triple2) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple7) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple7) -> (rule6 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((((triple7) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
((((triple7) -> (rule6 % int3)) ((((triple7) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
((((((triple7) -> (rule6 % int4)) ((((triple7) -> (rule6 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is round.
("Gary" "is" "round" "+")
((((((triple7) -> (rule6 % int5))) -> (rule4 % int4)) ((((((triple7) -> (rule6 % int5)) ((((triple7) -> (rule6 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5