Charlie is green. Charlie is rough. Harry is round. If Charlie is rough then Charlie is cold. If Harry is young and Harry is green then Harry is nice. If something is cold then it is furry. Furry, green things are nice. If something is furry and round then it is rough. Rough, cold things are green.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
If Charlie is rough then Charlie is cold.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "cold" "+"))
If Harry is young and Harry is green then Harry is nice.
((("Harry" "is" "young" "+") ("Harry" "is" "green" "+")) -> ("Harry" "is" "nice" "+"))
If something is cold then it is furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
Furry, green things are nice.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is furry and round then it is rough.
((("something" "is" "furry" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
Rough, cold things are green.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
Charlie is green.
True
1
proof
[(triple1 OR ((triple2 ((triple2) -> rule1)) -> rule6))]
("Charlie" "is" "green" "+")
triple1
((triple2 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not green.
False
1
inv-proof
[(triple1 OR ((triple2 ((triple2) -> rule1)) -> rule6))]
("Charlie" "is" "green" "-")
triple1
((triple2 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is cold.
True
2
proof
[(((triple2) -> rule1))]
("Charlie" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple2) -> rule1))]
("Charlie" "is" "cold" "-")
((triple2) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "furry" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not furry.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Charlie" "is" "furry" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
True
5
proof
[(((((((triple2) -> rule1)) -> rule3) triple1) -> rule4) OR ((((((triple2) -> rule1)) -> rule3) ((triple2 ((triple2) -> rule1)) -> rule6)) -> rule4))]
("Charlie" "is" "nice" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((((triple2) -> (rule1 % int4))) -> (rule3 % int3)) ((triple2 ((triple2) -> (rule1 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Charlie is not nice.
False
5
inv-proof
[(((((((triple2) -> rule1)) -> rule3) triple1) -> rule4) OR ((((((triple2) -> rule1)) -> rule3) ((triple2 ((triple2) -> rule1)) -> rule6)) -> rule4))]
("Charlie" "is" "nice" "-")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((((triple2) -> (rule1 % int4))) -> (rule3 % int3)) ((triple2 ((triple2) -> (rule1 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4
Harry is not rough.
Unknown
inv-rconc
[@2: Harry is rough.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is nice.
Unknown
rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Harry" "is" "nice" "+")
Harry is not furry.
Unknown
inv-rconc
[@1: Harry is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "green" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Charlie is green.[(triple1 OR ((triple2 ((triple2) -> rule1)) -> rule6))] Charlie is rough.[(triple2)] Harry is round.[(triple3)] @1: Charlie is cold.[(((triple2) -> rule1))] @2: Charlie is furry.[(((((triple2) -> rule1)) -> rule3))] @3: Charlie is nice.[(((((((triple2) -> rule1)) -> rule3) triple1) -> rule4) OR ((((((triple2) -> rule1)) -> rule3) ((triple2 ((triple2) -> rule1)) -> rule6)) -> rule4))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
((triple2 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple2) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
int3
((((((triple2) -> (rule1 % int4))) -> (rule3 % int3)) ((triple2 ((triple2) -> (rule1 % int4))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
int4