Dave is quiet. Fiona is quiet. Gary is quiet. Harry is blue. Red, blue things are not quiet. If something is quiet then it is not blue. If something is quiet then it is not red. If something is young and not blue then it is not rough. If something is quiet and not blue then it is young. All rough, white things are kind.
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Red, blue things are not quiet.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "-"))
If something is quiet then it is not blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "-"))
If something is quiet then it is not red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "-"))
If something is young and not blue then it is not rough.
((("something" "is" "young" "+") ("something" "is" "blue" "~")) -> ("something" "is" "rough" "-"))
If something is quiet and not blue then it is young.
((("something" "is" "quiet" "+") ("something" "is" "blue" "~")) -> ("something" "is" "young" "+"))
All rough, white things are kind.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Fiona is quiet.
True
1
proof
[(triple2)]
("Fiona" "is" "quiet" "+")
triple2
Dave is not quiet.
False
1
inv-proof
[(triple1)]
("Dave" "is" "quiet" "-")
triple1
Gary is not red.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "red" "-")
((triple3) -> (rule3 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Dave is red.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "red" "+")
((triple1) -> (rule3 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Dave is young.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule5))]
("Dave" "is" "young" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
int2
Gary is not young.
False
4
inv-proof
[(((triple3 ((triple3) -> rule2)) -> rule5))]
("Gary" "is" "young" "-")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not blue.
("Gary" "is" "blue" "-")
int2
Gary is not rough.
True
7
proof
[(((((triple3 ((triple3) -> rule2)) -> rule5) ((triple3) -> rule2)) -> rule4))]
("Gary" "is" "rough" "-")
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule5 % int2)) ((triple3) -> (rule2 % int3))) -> (rule4 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not blue.
("Gary" "is" "blue" "-")
int3
Fiona is rough.
False
7
inv-proof
[(((((triple2 ((triple2) -> rule2)) -> rule5) ((triple2) -> rule2)) -> rule4))]
("Fiona" "is" "rough" "+")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((triple2) -> (rule2 % int3))) -> (rule4 % int1))
Fiona is not rough.
("Fiona" "is" "rough" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not blue.
("Fiona" "is" "blue" "-")
int3
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "kind" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "kind" "-")
Fiona is kind.
Unknown
rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "kind" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Dave is quiet.[(triple1)] Fiona is quiet.[(triple2)] Gary is quiet.[(triple3)] Harry is blue.[(triple4)] @1: Dave is not blue.[(((triple1) -> rule2))] Dave is not red.[(((triple1) -> rule3))] Fiona is not blue.[(((triple2) -> rule2))] Fiona is not red.[(((triple2) -> rule3))] Gary is not blue.[(((triple3) -> rule2))] Gary is not red.[(((triple3) -> rule3))] @2: Dave is young.[(((triple1 ((triple1) -> rule2)) -> rule5))] Fiona is young.[(((triple2 ((triple2) -> rule2)) -> rule5))] Gary is young.[(((triple3 ((triple3) -> rule2)) -> rule5))] @3: Dave is not rough.[(((((triple1 ((triple1) -> rule2)) -> rule5) ((triple1) -> rule2)) -> rule4))] Fiona is not rough.[(((((triple2 ((triple2) -> rule2)) -> rule5) ((triple2) -> rule2)) -> rule4))] Gary is not rough.[(((((triple3 ((triple3) -> rule2)) -> rule5) ((triple3) -> rule2)) -> rule4))]
Dave is quiet.
("Dave" "is" "quiet" "+")
triple1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Dave is not blue.
("Dave" "is" "blue" "-")
((triple1) -> (rule2 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is not red.
("Dave" "is" "red" "-")
((triple1) -> (rule3 % int1))
Dave is not red.
("Dave" "is" "red" "-")
int1
Fiona is not blue.
("Fiona" "is" "blue" "-")
((triple2) -> (rule2 % int1))
Fiona is not blue.
("Fiona" "is" "blue" "-")
int1
Fiona is not red.
("Fiona" "is" "red" "-")
((triple2) -> (rule3 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Gary is not blue.
("Gary" "is" "blue" "-")
((triple3) -> (rule2 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Gary is not red.
("Gary" "is" "red" "-")
((triple3) -> (rule3 % int1))
Gary is not red.
("Gary" "is" "red" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
int2
Fiona is young.
("Fiona" "is" "young" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is not blue.
("Fiona" "is" "blue" "-")
int2
Gary is young.
("Gary" "is" "young" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not blue.
("Gary" "is" "blue" "-")
int2
Dave is not rough.
("Dave" "is" "rough" "-")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule5 % int2)) ((triple1) -> (rule2 % int3))) -> (rule4 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not blue.
("Dave" "is" "blue" "-")
int3
Fiona is not rough.
("Fiona" "is" "rough" "-")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule5 % int2)) ((triple2) -> (rule2 % int3))) -> (rule4 % int1))
Fiona is not rough.
("Fiona" "is" "rough" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is not blue.
("Fiona" "is" "blue" "-")
int3
Gary is not rough.
("Gary" "is" "rough" "-")
((((triple3 ((triple3) -> (rule2 % int3))) -> (rule5 % int2)) ((triple3) -> (rule2 % int3))) -> (rule4 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not blue.
("Gary" "is" "blue" "-")
int3