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