Anne is quiet. Anne is round. Anne is smart. Fiona is blue. Fiona is nice. Fiona is round. Fiona is smart. Fiona is young. Harry is blue. Harry is kind. Harry is quiet. Harry is smart. If someone is quiet and young then they are blue. Young people are smart. If someone is round and quiet then they are kind. If Anne is round then Anne is nice. All nice people are young. All quiet, young people are kind.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is quiet and young then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
Young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
If someone is round and quiet then they are kind.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If Anne is round then Anne is nice.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "nice" "+"))
All nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
All quiet, young people are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Fiona is young.
True
1
proof
[(triple8 OR ((triple5) -> rule5))]
("Fiona" "is" "young" "+")
triple8
((triple5) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is not blue.
False
1
inv-proof
[(triple9)]
("Harry" "is" "blue" "-")
triple9
Anne is nice.
True
2
proof
[(((triple2) -> rule4))]
("Anne" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple2) -> rule4))]
("Anne" "is" "nice" "-")
((triple2) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("Anne" "is" "young" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("Anne" "is" "young" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
True
5
proof
[(((triple1 ((((triple2) -> rule4)) -> rule5)) -> rule1))]
("Anne" "is" "blue" "+")
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not blue.
False
5
inv-proof
[(((triple1 ((((triple2) -> rule4)) -> rule5)) -> rule1))]
("Anne" "is" "blue" "-")
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "young" "-")
Fiona is kind.
Unknown
rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Anne is quiet.[(triple1)] Anne is round.[(triple2)] Anne is smart.[(triple3 OR ((((((triple2) -> rule4)) -> rule5)) -> rule2))] Fiona is blue.[(triple4)] Fiona is nice.[(triple5)] Fiona is round.[(triple6)] Fiona is smart.[(triple7 OR ((triple8) -> rule2) OR ((((triple5) -> rule5)) -> rule2))] Fiona is young.[(triple8 OR ((triple5) -> rule5))] Harry is blue.[(triple9)] Harry is kind.[(triple10)] Harry is quiet.[(triple11)] Harry is smart.[(triple12)] @1: Anne is kind.[(((triple2 triple1) -> rule3) OR ((triple1 ((((triple2) -> rule4)) -> rule5)) -> rule6))] Anne is nice.[(((triple2) -> rule4))] @2: Anne is young.[(((((triple2) -> rule4)) -> rule5))] @3: Anne is blue.[(((triple1 ((((triple2) -> rule4)) -> rule5)) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
triple4
Fiona is nice.
("Fiona" "is" "nice" "+")
triple5
Fiona is round.
("Fiona" "is" "round" "+")
triple6
Fiona is smart.
("Fiona" "is" "smart" "+")
triple7
((triple8) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
triple8
((triple5) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Anne is kind.
("Anne" "is" "kind" "+")
((triple2 triple1) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3