Dave is white. Fiona is young. If something is smart then it is not young. White things are big. If something is kind and white then it is big. If something is kind and smart then it is rough. If something is quiet and not white then it is smart. All big things are smart.
Dave is white.
("Dave" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If something is smart then it is not young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "-"))
White things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is kind and white then it is big.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If something is kind and smart then it is rough.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "rough" "+"))
If something is quiet and not white then it is smart.
((("something" "is" "quiet" "+") ("something" "is" "white" "~")) -> ("something" "is" "smart" "+"))
All big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Fiona is young.
True
1
proof
[(triple2)]
("Fiona" "is" "young" "+")
triple2
Dave is not white.
False
1
inv-proof
[(triple1)]
("Dave" "is" "white" "-")
triple1
Dave is big.
True
2
proof
[(((triple1) -> rule2))]
("Dave" "is" "big" "+")
((triple1) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Dave" "is" "big" "-")
((triple1) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("Dave" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not smart.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("Dave" "is" "smart" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not young.
True
4
proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule1))]
("Dave" "is" "young" "-")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is young.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule6)) -> rule1))]
("Dave" "is" "young" "+")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "rough" "-")
Fiona is smart.
Unknown
rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "big" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Dave is white.[(triple1)] Fiona is young.[(triple2)] @1: Dave is big.[(((triple1) -> rule2))] @2: Dave is smart.[(((((triple1) -> rule2)) -> rule6))] @3: Dave is not young.[(((((((triple1) -> rule2)) -> rule6)) -> rule1))]
Dave is white.
("Dave" "is" "white" "+")
triple1
Fiona is young.
("Fiona" "is" "young" "+")
triple2
Dave is big.
("Dave" "is" "big" "+")
((triple1) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not young.
("Dave" "is" "young" "-")
((((((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3