Charlie is big. Charlie is quiet. Charlie is rough. Charlie is round. Charlie is smart. Fiona is quiet. Fiona is young. If something is furry then it is quiet. Smart things are big. Young things are not furry. All quiet things are young. Round things are rough. If Fiona is round then Fiona is rough.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
Smart things are big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "+"))
Young things are not furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "-"))
All quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
Round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If Fiona is round then Fiona is rough.
((("Fiona" "is" "round" "+")) -> ("Fiona" "is" "rough" "+"))
Fiona is young.
True
1
proof
[(triple7 OR ((triple6) -> rule4))]
("Fiona" "is" "young" "+")
triple7
((triple6) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is not young.
False
1
inv-proof
[(triple7 OR ((triple6) -> rule4))]
("Fiona" "is" "young" "-")
triple7
((triple6) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Fiona is not furry.
True
2
proof
[(((triple7) -> rule3) OR ((((triple6) -> rule4)) -> rule3))]
("Fiona" "is" "furry" "-")
((triple7) -> (rule3 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Fiona is furry.
False
2
inv-proof
[(((triple7) -> rule3) OR ((((triple6) -> rule4)) -> rule3))]
("Fiona" "is" "furry" "+")
((triple7) -> (rule3 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Charlie is not furry.
True
3
proof
[(((((triple2) -> rule4)) -> rule3))]
("Charlie" "is" "furry" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule3))]
("Charlie" "is" "furry" "+")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Charlie is big.[(triple1 OR ((triple5) -> rule2))] Charlie is quiet.[(triple2)] Charlie is rough.[(triple3 OR ((triple4) -> rule5))] Charlie is round.[(triple4)] Charlie is smart.[(triple5)] Fiona is quiet.[(triple6)] Fiona is young.[(triple7 OR ((triple6) -> rule4))] @1: Charlie is young.[(((triple2) -> rule4))] Fiona is not furry.[(((triple7) -> rule3) OR ((((triple6) -> rule4)) -> rule3))] @2: Charlie is not furry.[(((((triple2) -> rule4)) -> rule3))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple5) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
((triple4) -> (rule5 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple6
Fiona is young.
("Fiona" "is" "young" "+")
triple7
((triple6) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple2) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Fiona is not furry.
("Fiona" "is" "furry" "-")
((triple7) -> (rule3 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is not furry.
("Fiona" "is" "furry" "-")
int1
Fiona is young.
("Fiona" "is" "young" "+")
int2
Charlie is not furry.
("Charlie" "is" "furry" "-")
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2