Charlie is quiet. Fiona is red. All smart, quiet people are red. If someone is quiet then they are big. Quiet people are white. If someone is kind and quiet then they are rough. If someone is smart then they are kind. Quiet, big people are smart.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Fiona is red.
("Fiona" "is" "red" "+")
All smart, quiet people are red.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If someone is quiet then they are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is kind and quiet then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Quiet, big people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Charlie is quiet.
True
1
proof
[(triple1)]
("Charlie" "is" "quiet" "+")
triple1
Charlie is not quiet.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "quiet" "-")
triple1
Charlie is big.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "big" "+")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "white" "-")
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule6))]
("Charlie" "is" "smart" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not smart.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule6))]
("Charlie" "is" "smart" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is red.
True
6
proof
[(((((triple1 ((triple1) -> rule2)) -> rule6) triple1) -> rule1))]
("Charlie" "is" "red" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not kind.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule5))]
("Charlie" "is" "kind" "-")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Fiona is not smart.
Unknown
inv-rconc
[@1: Fiona is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "white" "-")
Fiona is rough.
Unknown
rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "rough" "+")
@0: Charlie is quiet.[(triple1)] Fiona is red.[(triple2)] @1: Charlie is big.[(((triple1) -> rule2))] Charlie is white.[(((triple1) -> rule3))] @2: Charlie is smart.[(((triple1 ((triple1) -> rule2)) -> rule6))] @3: Charlie is kind.[(((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule5))] Charlie is red.[(((((triple1 ((triple1) -> rule2)) -> rule6) triple1) -> rule1))] @4: Charlie is rough.[(((((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule5) triple1) -> rule4))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Fiona is red.
("Fiona" "is" "red" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple1 ((triple1) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule5 % int2)) triple1) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4