Dave is blue. Dave is green. Dave is not quiet. Dave is red. Fiona is blue. Fiona is red. Gary is not blue. Gary is kind. Gary is quiet. Gary is white. Gary is not young. Harry is green. Harry is quiet. Harry is red. Harry is young. Quiet, red people are blue. If Fiona is kind then Fiona is not quiet. If someone is kind and not white then they are not quiet. All blue people are green. If Fiona is green then Fiona is not young. If someone is green then they are red.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is red.
("Dave" "is" "red" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is not young.
("Gary" "is" "young" "-")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
Quiet, red people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If Fiona is kind then Fiona is not quiet.
((("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "quiet" "-"))
If someone is kind and not white then they are not quiet.
((("someone" "is" "kind" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "quiet" "-"))
All blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If Fiona is green then Fiona is not young.
((("Fiona" "is" "green" "+")) -> ("Fiona" "is" "young" "-"))
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Gary is quiet.
True
1
proof
[(triple9)]
("Gary" "is" "quiet" "+")
triple9
Harry is not quiet.
False
1
inv-proof
[(triple13)]
("Harry" "is" "quiet" "-")
triple13
Harry is blue.
True
3
proof
[(((triple13 triple14) -> rule1) OR ((triple13 ((triple12) -> rule6)) -> rule1))]
("Harry" "is" "blue" "+")
((triple13 triple14) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple13 ((triple12) -> (rule6 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not blue.
False
3
inv-proof
[(((triple13 triple14) -> rule1) OR ((triple13 ((triple12) -> rule6)) -> rule1))]
("Harry" "is" "blue" "-")
((triple13 triple14) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple13 ((triple12) -> (rule6 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Fiona is not young.
True
3
proof
[(((((triple5) -> rule4)) -> rule5))]
("Fiona" "is" "young" "-")
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is young.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule5))]
("Fiona" "is" "young" "+")
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is red.
Unknown
rconc
[@2: Gary is red.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Gary" "is" "red" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Dave is blue.[(triple1)] Dave is green.[(triple2 OR ((triple1) -> rule4))] Dave is not quiet.[(triple3)] Dave is red.[(triple4 OR ((triple2) -> rule6) OR ((((triple1) -> rule4)) -> rule6))] Fiona is blue.[(triple5)] Fiona is red.[(triple6 OR ((((triple5) -> rule4)) -> rule6))] Gary is kind.[(triple8)] Gary is not blue.[(triple7)] Gary is not young.[(triple11)] Gary is quiet.[(triple9)] Gary is white.[(triple10)] Harry is green.[(triple12 OR ((((triple13 triple14) -> rule1)) -> rule4))] Harry is quiet.[(triple13)] Harry is red.[(triple14 OR ((triple12) -> rule6))] Harry is young.[(triple15)] @1: Fiona is green.[(((triple5) -> rule4))] Harry is blue.[(((triple13 triple14) -> rule1) OR ((triple13 ((triple12) -> rule6)) -> rule1))] @2: Fiona is not young.[(((((triple5) -> rule4)) -> rule5))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is green.
("Dave" "is" "green" "+")
triple2
((triple1) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
((triple2) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
Fiona is red.
("Fiona" "is" "red" "+")
triple6
((((triple5) -> (rule4 % int2))) -> (rule6 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple8
Gary is not blue.
("Gary" "is" "blue" "-")
triple7
Gary is not young.
("Gary" "is" "young" "-")
triple11
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
triple12
((((triple13 triple14) -> (rule1 % int2))) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is red.
("Harry" "is" "red" "+")
triple14
((triple12) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple15
Fiona is green.
("Fiona" "is" "green" "+")
((triple5) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple13 triple14) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple13 ((triple12) -> (rule6 % int2))) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Fiona is not young.
("Fiona" "is" "young" "-")
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2