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