Bob is blue. Bob is smart. Bob is white. Bob is young. Fiona is blue. Fiona is not nice. Fiona is quiet. Fiona is red. Fiona is white. Harry is not blue. Harry is red. Harry is smart. If something is smart and not blue then it is white. If something is white and smart then it is young. If something is blue and not nice then it is quiet. If something is smart and not blue then it is quiet. If something is blue and not white then it is not quiet. All nice, red things are quiet.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is not nice.
("Fiona" "is" "nice" "-")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is not blue.
("Harry" "is" "blue" "-")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is smart and not blue then it is white.
((("something" "is" "smart" "+") ("something" "is" "blue" "~")) -> ("something" "is" "white" "+"))
If something is white and smart then it is young.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If something is blue and not nice then it is quiet.
((("something" "is" "blue" "+") ("something" "is" "nice" "~")) -> ("something" "is" "quiet" "+"))
If something is smart and not blue then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "blue" "~")) -> ("something" "is" "quiet" "+"))
If something is blue and not white then it is not quiet.
((("something" "is" "blue" "+") ("something" "is" "white" "~")) -> ("something" "is" "quiet" "-"))
All nice, red things are quiet.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Harry is smart.
True
1
proof
[(triple12)]
("Harry" "is" "smart" "+")
triple12
Fiona is not quiet.
False
1
inv-proof
[(triple7 OR ((triple5 triple6) -> rule3))]
("Fiona" "is" "quiet" "-")
triple7
((triple5 triple6) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Harry is quiet.
True
3
proof
[(((triple12 triple10) -> rule4))]
("Harry" "is" "quiet" "+")
((triple12 triple10) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
3
inv-proof
[(((triple12 triple10) -> rule4))]
("Harry" "is" "quiet" "-")
((triple12 triple10) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
True
5
proof
[(((((triple12 triple10) -> rule1) triple12) -> rule2))]
("Harry" "is" "young" "+")
((((triple12 triple10) -> (rule1 % int2)) triple12) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not young.
False
5
inv-proof
[(((((triple12 triple10) -> rule1) triple12) -> rule2))]
("Harry" "is" "young" "-")
((((triple12 triple10) -> (rule1 % int2)) triple12) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "quiet" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "young" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Bob is blue.[(triple1)] Bob is smart.[(triple2)] Bob is white.[(triple3)] Bob is young.[(triple4 OR ((triple3 triple2) -> rule2))] Fiona is blue.[(triple5)] Fiona is not nice.[(triple6)] Fiona is quiet.[(triple7 OR ((triple5 triple6) -> rule3))] Fiona is red.[(triple8)] Fiona is white.[(triple9)] Harry is not blue.[(triple10)] Harry is red.[(triple11)] Harry is smart.[(triple12)] @1: Harry is quiet.[(((triple12 triple10) -> rule4))] Harry is white.[(((triple12 triple10) -> rule1))] @2: Harry is young.[(((((triple12 triple10) -> rule1) triple12) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
((triple3 triple2) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
Fiona is not nice.
("Fiona" "is" "nice" "-")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
((triple5 triple6) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple8
Fiona is white.
("Fiona" "is" "white" "+")
triple9
Harry is not blue.
("Harry" "is" "blue" "-")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple12 triple10) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple12 triple10) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple12 triple10) -> (rule1 % int2)) triple12) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2