Anne is kind. Dave is red. Fiona is smart. Harry is round. If something is big and not round then it is kind. Smart, rough things are kind. If something is rough and kind then it is young. If something is smart then it is rough. If something is smart and not round then it is big. If something is round then it is big.
Anne is kind.
("Anne" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is big and not round then it is kind.
((("something" "is" "big" "+") ("something" "is" "round" "~")) -> ("something" "is" "kind" "+"))
Smart, rough things are kind.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is rough and kind then it is young.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is smart then it is rough.
((("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is smart and not round then it is big.
((("something" "is" "smart" "+") ("something" "is" "round" "~")) -> ("something" "is" "big" "+"))
If something is round then it is big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Harry is round.
True
1
proof
[(triple4)]
("Harry" "is" "round" "+")
triple4
Harry is not round.
False
1
inv-proof
[(triple4)]
("Harry" "is" "round" "-")
triple4
Fiona is rough.
True
2
proof
[(((triple3) -> rule4))]
("Fiona" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple4) -> rule6))]
("Harry" "is" "big" "-")
((triple4) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Fiona is kind.
True
4
proof
[(((triple3 ((triple3) -> rule4)) -> rule2))]
("Fiona" "is" "kind" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not kind.
False
4
inv-proof
[(((triple3 ((triple3) -> rule4)) -> rule2))]
("Fiona" "is" "kind" "-")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is young.
True
7
proof
[(((((triple3) -> rule4) ((triple3 ((triple3) -> rule4)) -> rule2)) -> rule3))]
("Fiona" "is" "young" "+")
((((triple3) -> (rule4 % int3)) ((triple3 ((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is not young.
False
7
inv-proof
[(((((triple3) -> rule4) ((triple3 ((triple3) -> rule4)) -> rule2)) -> rule3))]
("Fiona" "is" "young" "-")
((((triple3) -> (rule4 % int3)) ((triple3 ((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "big" "-")
Harry is young.
Unknown
rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Harry" "is" "young" "+")
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "kind" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "big" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is kind.[(triple1)] Dave is red.[(triple2)] Fiona is smart.[(triple3)] Harry is round.[(triple4)] @1: Fiona is rough.[(((triple3) -> rule4))] Harry is big.[(((triple4) -> rule6))] @2: Fiona is kind.[(((triple3 ((triple3) -> rule4)) -> rule2))] @3: Fiona is young.[(((((triple3) -> rule4) ((triple3 ((triple3) -> rule4)) -> rule2)) -> rule3))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple3) -> (rule4 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple4) -> (rule6 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple3 ((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((((triple3) -> (rule4 % int3)) ((triple3 ((triple3) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3