Dave is rough. Fiona is smart. Gary is young. If Gary is big and Gary is kind then Gary is not young. If Gary is not blue then Gary is not young. If someone is smart then they are kind. If Fiona is young and Fiona is kind then Fiona is big. If someone is quiet then they are not big. Blue, kind people are not young. All quiet people are rough. Kind people are quiet.
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
If Gary is big and Gary is kind then Gary is not young.
((("Gary" "is" "big" "+") ("Gary" "is" "kind" "+")) -> ("Gary" "is" "young" "-"))
If Gary is not blue then Gary is not young.
((("Gary" "is" "blue" "~")) -> ("Gary" "is" "young" "-"))
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
If Fiona is young and Fiona is kind then Fiona is big.
((("Fiona" "is" "young" "+") ("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "big" "+"))
If someone is quiet then they are not big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "-"))
Blue, kind people are not young.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "-"))
All quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
Kind people are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Gary is young.
True
1
proof
[(triple3)]
("Gary" "is" "young" "+")
triple3
Gary is not young.
False
1
inv-proof
[(triple3)]
("Gary" "is" "young" "-")
triple3
Fiona is kind.
True
2
proof
[(((triple2) -> rule3))]
("Fiona" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is not kind.
False
2
inv-proof
[(((triple2) -> rule3))]
("Fiona" "is" "kind" "-")
((triple2) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
True
3
proof
[(((((triple2) -> rule3)) -> rule8))]
("Fiona" "is" "quiet" "+")
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not quiet.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule8))]
("Fiona" "is" "quiet" "-")
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not big.
True
4
proof
[(((((((triple2) -> rule3)) -> rule8)) -> rule5))]
("Fiona" "is" "big" "-")
((((((triple2) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Fiona is not big.
("Fiona" "is" "big" "-")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is not rough.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule8)) -> rule7))]
("Fiona" "is" "rough" "-")
((((((triple2) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "kind" "-")
Dave is quiet.
Unknown
rconc
[@2: Dave is quiet.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("Dave" "is" "quiet" "+")
Gary is not quiet.
Unknown
inv-rconc
[@2: Gary is quiet.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is rough.
Unknown
rconc
[@3: Gary is rough.[CWA. Example of deepest failure = (rule7 <- rule8 <- rule3 <- FAIL)]]
("Gary" "is" "rough" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Dave is rough.[(triple1)] Fiona is smart.[(triple2)] Gary is young.[(triple3)] @1: Fiona is kind.[(((triple2) -> rule3))] @2: Fiona is quiet.[(((((triple2) -> rule3)) -> rule8))] @3: Fiona is not big.[(((((((triple2) -> rule3)) -> rule8)) -> rule5))] Fiona is rough.[(((((((triple2) -> rule3)) -> rule8)) -> rule7))]
Dave is rough.
("Dave" "is" "rough" "+")
triple1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple2) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not big.
("Fiona" "is" "big" "-")
((((((triple2) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
Fiona is not big.
("Fiona" "is" "big" "-")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
((((((triple2) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
int3