Charlie is kind. Dave is blue. Dave is kind. Dave is quiet. Fiona is big. Fiona is young. Harry is quiet. If something is quiet then it is kind. All white things are quiet. If something is white then it is blue. Smart, quiet things are blue. All young, quiet things are white. Smart things are big. All smart, blue things are quiet. Blue things are young.
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is quiet then it is kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
All white things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is white then it is blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Smart, quiet things are blue.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
All young, quiet things are white.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
All smart, blue things are quiet.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Dave is blue.
True
1
proof
[(triple2)]
("Dave" "is" "blue" "+")
triple2
Fiona is not big.
False
1
inv-proof
[(triple5)]
("Fiona" "is" "big" "-")
triple5
Harry is kind.
True
2
proof
[(((triple7) -> rule1))]
("Harry" "is" "kind" "+")
((triple7) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple7) -> rule1))]
("Harry" "is" "kind" "-")
((triple7) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Dave is white.
True
4
proof
[(((((triple2) -> rule8) triple4) -> rule5))]
("Dave" "is" "white" "+")
((((triple2) -> (rule8 % int2)) triple4) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not white.
False
4
inv-proof
[(((((triple2) -> rule8) triple4) -> rule5))]
("Dave" "is" "white" "-")
((((triple2) -> (rule8 % int2)) triple4) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Harry is not white.
Unknown
inv-rconc
[@3: Harry is white.[CWA. Example of deepest failure = (rule5 <- rule8 <- rule3 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is young.
Unknown
rconc
[@3: Harry is young.[CWA. Example of deepest failure = (rule8 <- rule3 <- rule5 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not blue.
Unknown
inv-rconc
[@4: Harry is blue.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule8 <- rule4 <- FAIL)]]
("Harry" "is" "blue" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is kind.[(triple1)] Dave is blue.[(triple2)] Dave is kind.[(triple3 OR ((triple4) -> rule1))] Dave is quiet.[(triple4)] Fiona is big.[(triple5)] Fiona is young.[(triple6)] Harry is quiet.[(triple7)] @1: Dave is young.[(((triple2) -> rule8))] Harry is kind.[(((triple7) -> rule1))] @2: Dave is white.[(((((triple2) -> rule8) triple4) -> rule5))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
((triple4) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Fiona is big.
("Fiona" "is" "big" "+")
triple5
Fiona is young.
("Fiona" "is" "young" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
((triple2) -> (rule8 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple7) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((((triple2) -> (rule8 % int2)) triple4) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2