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