Anne is rough. Dave is big. Dave is smart. Fiona is big. Fiona is rough. Fiona is white. Gary is kind. Smart things are young. If something is kind then it is young. If something is young then it is kind. All kind things are white. If something is furry and smart then it is white. If Fiona is furry and Fiona is rough then Fiona is big. Rough things are big. All big things are smart.
Anne is rough.
("Anne" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If something is kind then it is young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is young then it is kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If something is furry and smart then it is white.
((("something" "is" "furry" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If Fiona is furry and Fiona is rough then Fiona is big.
((("Fiona" "is" "furry" "+") ("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "big" "+"))
Rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
All big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Dave is smart.
True
1
proof
[(triple3 OR ((triple2) -> rule8))]
("Dave" "is" "smart" "+")
triple3
((triple2) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Fiona is not big.
False
1
inv-proof
[(triple4 OR ((triple5) -> rule7))]
("Fiona" "is" "big" "-")
triple4
((triple5) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Dave is young.
True
2
proof
[(((triple3) -> rule1) OR ((((triple2) -> rule8)) -> rule1))]
("Dave" "is" "young" "+")
((triple3) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple2) -> (rule8 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Fiona is not smart.
False
2
inv-proof
[(((triple4) -> rule8) OR ((((triple5) -> rule7)) -> rule8))]
("Fiona" "is" "smart" "-")
((triple4) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple5) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Dave is kind.
True
3
proof
[(((((triple3) -> rule1)) -> rule3) OR ((((((triple2) -> rule8)) -> rule1)) -> rule3))]
("Dave" "is" "kind" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((((triple2) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Fiona is not young.
False
3
inv-proof
[(((((triple4) -> rule8)) -> rule1) OR ((((((triple5) -> rule7)) -> rule8)) -> rule1))]
("Fiona" "is" "young" "-")
((((triple4) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((triple5) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Anne is young.
True
4
proof
[(((((((triple1) -> rule7)) -> rule8)) -> rule1))]
("Anne" "is" "young" "+")
((((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Dave is not white.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule3)) -> rule4) OR ((((((((triple2) -> rule8)) -> rule1)) -> rule3)) -> rule4))]
("Dave" "is" "white" "-")
((((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((((((triple2) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Anne is kind.
True
5
proof
[(((((((((triple1) -> rule7)) -> rule8)) -> rule1)) -> rule3))]
("Anne" "is" "kind" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is not kind.
False
5
inv-proof
[(((((((((triple1) -> rule7)) -> rule8)) -> rule1)) -> rule3))]
("Anne" "is" "kind" "-")
((((((((triple1) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is white.
True
6
proof
[(((((((((((triple1) -> rule7)) -> rule8)) -> rule1)) -> rule3)) -> rule4))]
("Anne" "is" "white" "+")
((((((((((triple1) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
Anne is not white.
False
6
inv-proof
[(((((((((((triple1) -> rule7)) -> rule8)) -> rule1)) -> rule3)) -> rule4))]
("Anne" "is" "white" "-")
((((((((((triple1) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5
Gary is not smart.
Unknown
inv-rconc
[@2: Gary is smart.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "big" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Anne is rough.[(triple1)] Dave is big.[(triple2)] Dave is smart.[(triple3 OR ((triple2) -> rule8))] Fiona is big.[(triple4 OR ((triple5) -> rule7))] Fiona is rough.[(triple5)] Fiona is white.[(triple6 OR ((((((((triple4) -> rule8)) -> rule1)) -> rule3)) -> rule4) OR ((((((((((triple5) -> rule7)) -> rule8)) -> rule1)) -> rule3)) -> rule4))] Gary is kind.[(triple7)] @1: Anne is big.[(((triple1) -> rule7))] Dave is young.[(((triple3) -> rule1) OR ((((triple2) -> rule8)) -> rule1))] Fiona is smart.[(((triple4) -> rule8) OR ((((triple5) -> rule7)) -> rule8))] Gary is white.[(((triple7) -> rule4))] Gary is young.[(((triple7) -> rule2))] @2: Anne is smart.[(((((triple1) -> rule7)) -> rule8))] Dave is kind.[(((((triple3) -> rule1)) -> rule3) OR ((((((triple2) -> rule8)) -> rule1)) -> rule3))] Fiona is young.[(((((triple4) -> rule8)) -> rule1) OR ((((((triple5) -> rule7)) -> rule8)) -> rule1))] @3: Anne is young.[(((((((triple1) -> rule7)) -> rule8)) -> rule1))] Dave is white.[(((((((triple3) -> rule1)) -> rule3)) -> rule4) OR ((((((((triple2) -> rule8)) -> rule1)) -> rule3)) -> rule4))] Fiona is kind.[(((((((triple4) -> rule8)) -> rule1)) -> rule3) OR ((((((((triple5) -> rule7)) -> rule8)) -> rule1)) -> rule3))] @4: Anne is kind.[(((((((((triple1) -> rule7)) -> rule8)) -> rule1)) -> rule3))] @5: Anne is white.[(((((((((((triple1) -> rule7)) -> rule8)) -> rule1)) -> rule3)) -> rule4))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
((triple2) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
triple4
((triple5) -> (rule7 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple5
Fiona is white.
("Fiona" "is" "white" "+")
triple6
((((((((triple4) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
((((((((((triple5) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
int4
Fiona is big.
("Fiona" "is" "big" "+")
int5
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule7 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple3) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple2) -> (rule8 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple4) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple5) -> (rule7 % int2))) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple7) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple7) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((((triple2) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Fiona is young.
("Fiona" "is" "young" "+")
((((triple4) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((((triple5) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
((((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((((((triple2) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
((((((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
((((((((triple5) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is smart.
("Fiona" "is" "smart" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
int4
Anne is kind.
("Anne" "is" "kind" "+")
((((((((triple1) -> (rule7 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
int4
Anne is white.
("Anne" "is" "white" "+")
((((((((((triple1) -> (rule7 % int5))) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is big.
("Anne" "is" "big" "+")
int5