Anne is kind. Anne is white. Bob is blue. Bob is young. Fiona is furry. Fiona is kind. Fiona is not white. Harry is blue. Harry is not kind. Harry is quiet. Harry is white. All kind things are young. All white, quiet things are blue. If Harry is nice then Harry is blue. If Harry is nice then Harry is furry. Young things are quiet. If something is blue then it is white. All blue things are nice. Blue, nice things are furry. If something is blue and not young then it is furry.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is young.
("Bob" "is" "young" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is not white.
("Fiona" "is" "white" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
All kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All white, quiet things are blue.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If Harry is nice then Harry is blue.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "blue" "+"))
If Harry is nice then Harry is furry.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "furry" "+"))
Young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If something is blue then it is white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
All blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Blue, nice things are furry.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If something is blue and not young then it is furry.
((("something" "is" "blue" "+") ("something" "is" "young" "~")) -> ("something" "is" "furry" "+"))
Bob is young.
True
1
proof
[(triple4)]
("Bob" "is" "young" "+")
triple4
Harry is not white.
False
1
inv-proof
[(triple11 OR ((triple8) -> rule6))]
("Harry" "is" "white" "-")
triple11
((triple8) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Anne is young.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "young" "+")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple3) -> rule6))]
("Bob" "is" "white" "-")
((triple3) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Anne is quiet.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((((triple8) -> rule7)) -> rule4) OR ((triple8 ((triple8) -> rule7)) -> rule8) OR ((((triple11 triple10) -> rule2) ((triple8) -> rule7)) -> rule8) OR ((((((triple11 triple10) -> rule2)) -> rule7)) -> rule4) OR ((triple8 ((((triple11 triple10) -> rule2)) -> rule7)) -> rule8) OR ((((triple11 triple10) -> rule2) ((((triple11 triple10) -> rule2)) -> rule7)) -> rule8))]
("Harry" "is" "furry" "-")
((((triple8) -> (rule7 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple8 ((triple8) -> (rule7 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple11 triple10) -> (rule2 % int3)) ((triple8) -> (rule7 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple11 triple10) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((triple8 ((((triple11 triple10) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((triple11 triple10) -> (rule2 % int3)) ((((triple11 triple10) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Anne is blue.
True
5
proof
[(((triple2 ((((triple1) -> rule1)) -> rule5)) -> rule2))]
("Anne" "is" "blue" "+")
((triple2 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not blue.
False
5
inv-proof
[(((triple2 ((((triple1) -> rule1)) -> rule5)) -> rule2))]
("Anne" "is" "blue" "-")
((triple2 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is nice.
True
6
proof
[(((((triple2 ((((triple1) -> rule1)) -> rule5)) -> rule2)) -> rule7))]
("Anne" "is" "nice" "+")
((((triple2 ((((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is not nice.
False
6
inv-proof
[(((((triple2 ((((triple1) -> rule1)) -> rule5)) -> rule2)) -> rule7))]
("Anne" "is" "nice" "-")
((((triple2 ((((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is furry.
True
12
proof
[(((((triple2 ((((triple1) -> rule1)) -> rule5)) -> rule2) ((((triple2 ((((triple1) -> rule1)) -> rule5)) -> rule2)) -> rule7)) -> rule8))]
("Anne" "is" "furry" "+")
((((triple2 ((((triple1) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3)) ((((triple2 ((((triple1) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5
Anne is not furry.
False
12
inv-proof
[(((((triple2 ((((triple1) -> rule1)) -> rule5)) -> rule2) ((((triple2 ((((triple1) -> rule1)) -> rule5)) -> rule2)) -> rule7)) -> rule8))]
("Anne" "is" "furry" "-")
((((triple2 ((((triple1) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3)) ((((triple2 ((((triple1) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "young" "-")
Fiona is blue.
Unknown
rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "blue" "+")
Fiona is not nice.
Unknown
inv-rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("Fiona" "is" "nice" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Anne is white.[(triple2)] Bob is blue.[(triple3)] Bob is young.[(triple4)] Fiona is furry.[(triple5)] Fiona is kind.[(triple6)] Fiona is not white.[(triple7)] Harry is blue.[(triple8 OR ((triple11 triple10) -> rule2))] Harry is not kind.[(triple9)] Harry is quiet.[(triple10)] Harry is white.[(triple11 OR ((triple8) -> rule6))] @1: Anne is young.[(((triple1) -> rule1))] Bob is nice.[(((triple3) -> rule7))] Bob is quiet.[(((triple4) -> rule5))] Bob is white.[(((triple3) -> rule6))] Fiona is young.[(((triple6) -> rule1))] Harry is nice.[(((triple8) -> rule7) OR ((((triple11 triple10) -> rule2)) -> rule7))] @2: Anne is quiet.[(((((triple1) -> rule1)) -> rule5))] Bob is furry.[(((triple3 ((triple3) -> rule7)) -> rule8))] Fiona is quiet.[(((((triple6) -> rule1)) -> rule5))] Harry is furry.[(((((triple8) -> rule7)) -> rule4) OR ((triple8 ((triple8) -> rule7)) -> rule8) OR ((((triple11 triple10) -> rule2) ((triple8) -> rule7)) -> rule8) OR ((((((triple11 triple10) -> rule2)) -> rule7)) -> rule4) OR ((triple8 ((((triple11 triple10) -> rule2)) -> rule7)) -> rule8) OR ((((triple11 triple10) -> rule2) ((((triple11 triple10) -> rule2)) -> rule7)) -> rule8))] @3: Anne is blue.[(((triple2 ((((triple1) -> rule1)) -> rule5)) -> rule2))] @4: Anne is nice.[(((((triple2 ((((triple1) -> rule1)) -> rule5)) -> rule2)) -> rule7))] @5: Anne is furry.[(((((triple2 ((((triple1) -> rule1)) -> rule5)) -> rule2) ((((triple2 ((((triple1) -> rule1)) -> rule5)) -> rule2)) -> rule7)) -> rule8))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Fiona is furry.
("Fiona" "is" "furry" "+")
triple5
Fiona is kind.
("Fiona" "is" "kind" "+")
triple6
Fiona is not white.
("Fiona" "is" "white" "-")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
((triple11 triple10) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not kind.
("Harry" "is" "kind" "-")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is white.
("Harry" "is" "white" "+")
triple11
((triple8) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple3) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple4) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple3) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple6) -> (rule1 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((triple8) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple11 triple10) -> (rule2 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((triple3 ((triple3) -> (rule7 % int2))) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple6) -> (rule1 % int2))) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((triple8) -> (rule7 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((triple8 ((triple8) -> (rule7 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
((((triple11 triple10) -> (rule2 % int3)) ((triple8) -> (rule7 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((((triple11 triple10) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((triple8 ((((triple11 triple10) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((((triple11 triple10) -> (rule2 % int3)) ((((triple11 triple10) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
((triple2 ((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
((((triple2 ((((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
((((triple2 ((((triple1) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3)) ((((triple2 ((((triple1) -> (rule1 % int5))) -> (rule5 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5