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