Bob is furry. Bob is smart. Bob is white. Bob is young. Erin is kind. Fiona is furry. Fiona is quiet. Fiona is rough. Fiona is young. Gary is quiet. Gary is smart. Gary is young. Furry things are white. If something is rough and smart then it is furry. All kind, rough things are smart. If Fiona is kind then Fiona is furry. If Erin is quiet and Erin is white then Erin is kind. If Erin is white and Erin is kind then Erin is young. Kind things are rough.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Furry things are white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If something is rough and smart then it is furry.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
All kind, rough things are smart.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If Fiona is kind then Fiona is furry.
((("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "furry" "+"))
If Erin is quiet and Erin is white then Erin is kind.
((("Erin" "is" "quiet" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "kind" "+"))
If Erin is white and Erin is kind then Erin is young.
((("Erin" "is" "white" "+") ("Erin" "is" "kind" "+")) -> ("Erin" "is" "young" "+"))
Kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Fiona is young.
True
1
proof
[(triple9)]
("Fiona" "is" "young" "+")
triple9
Fiona is not young.
False
1
inv-proof
[(triple9)]
("Fiona" "is" "young" "-")
triple9
Erin is rough.
True
2
proof
[(((triple5) -> rule7))]
("Erin" "is" "rough" "+")
((triple5) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is not rough.
False
2
inv-proof
[(((triple5) -> rule7))]
("Erin" "is" "rough" "-")
((triple5) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
True
4
proof
[(((triple5 ((triple5) -> rule7)) -> rule3))]
("Erin" "is" "smart" "+")
((triple5 ((triple5) -> (rule7 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is not smart.
False
4
inv-proof
[(((triple5 ((triple5) -> rule7)) -> rule3))]
("Erin" "is" "smart" "-")
((triple5 ((triple5) -> (rule7 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
True
7
proof
[(((((triple5) -> rule7) ((triple5 ((triple5) -> rule7)) -> rule3)) -> rule2))]
("Erin" "is" "furry" "+")
((((triple5) -> (rule7 % int3)) ((triple5 ((triple5) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not furry.
False
7
inv-proof
[(((((triple5) -> rule7) ((triple5 ((triple5) -> rule7)) -> rule3)) -> rule2))]
("Erin" "is" "furry" "-")
((((triple5) -> (rule7 % int3)) ((triple5 ((triple5) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is white.
True
8
proof
[(((((((triple5) -> rule7) ((triple5 ((triple5) -> rule7)) -> rule3)) -> rule2)) -> rule1))]
("Erin" "is" "white" "+")
((((((triple5) -> (rule7 % int4)) ((triple5 ((triple5) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is not white.
False
8
inv-proof
[(((((((triple5) -> rule7) ((triple5 ((triple5) -> rule7)) -> rule3)) -> rule2)) -> rule1))]
("Erin" "is" "white" "-")
((((((triple5) -> (rule7 % int4)) ((triple5 ((triple5) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is young.
True
10
proof
[(((((((((triple5) -> rule7) ((triple5 ((triple5) -> rule7)) -> rule3)) -> rule2)) -> rule1) triple5) -> rule6))]
("Erin" "is" "young" "+")
((((((((triple5) -> (rule7 % int5)) ((triple5 ((triple5) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) triple5) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
int5
Erin is not young.
False
10
inv-proof
[(((((((((triple5) -> rule7) ((triple5 ((triple5) -> rule7)) -> rule3)) -> rule2)) -> rule1) triple5) -> rule6))]
("Erin" "is" "young" "-")
((((((((triple5) -> (rule7 % int5)) ((triple5 ((triple5) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) triple5) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
int5
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "rough" "-")
Fiona is smart.
Unknown
rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "smart" "+")
Gary is not furry.
Unknown
inv-rconc
[@2: Gary is furry.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("Gary" "is" "furry" "-")
Gary is white.
Unknown
rconc
[@3: Gary is white.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule7 <- FAIL)]]
("Gary" "is" "white" "+")
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "rough" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is furry.[(triple1)] Bob is smart.[(triple2)] Bob is white.[(triple3 OR ((triple1) -> rule1))] Bob is young.[(triple4)] Erin is kind.[(triple5)] Fiona is furry.[(triple6)] Fiona is quiet.[(triple7)] Fiona is rough.[(triple8)] Fiona is young.[(triple9)] Gary is quiet.[(triple10)] Gary is smart.[(triple11)] Gary is young.[(triple12)] @1: Erin is rough.[(((triple5) -> rule7))] Fiona is white.[(((triple6) -> rule1))] @2: Erin is smart.[(((triple5 ((triple5) -> rule7)) -> rule3))] @3: Erin is furry.[(((((triple5) -> rule7) ((triple5 ((triple5) -> rule7)) -> rule3)) -> rule2))] @4: Erin is white.[(((((((triple5) -> rule7) ((triple5 ((triple5) -> rule7)) -> rule3)) -> rule2)) -> rule1))] @5: Erin is young.[(((((((((triple5) -> rule7) ((triple5 ((triple5) -> rule7)) -> rule3)) -> rule2)) -> rule1) triple5) -> rule6))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Fiona is furry.
("Fiona" "is" "furry" "+")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Fiona is rough.
("Fiona" "is" "rough" "+")
triple8
Fiona is young.
("Fiona" "is" "young" "+")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Gary is smart.
("Gary" "is" "smart" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
Erin is rough.
("Erin" "is" "rough" "+")
((triple5) -> (rule7 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple6) -> (rule1 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple5 ((triple5) -> (rule7 % int2))) -> (rule3 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
((((triple5) -> (rule7 % int3)) ((triple5 ((triple5) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((((((triple5) -> (rule7 % int4)) ((triple5 ((triple5) -> (rule7 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
((((((((triple5) -> (rule7 % int5)) ((triple5 ((triple5) -> (rule7 % int5))) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) triple5) -> (rule6 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
int5