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