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